Michael Norrish
Michael Norrish
The `[foo:]` syntax should be able to stand in for conjunctions separating clauses. This would require the quotation-filter to look for non-comment, non-whitespace characters occurring after conjunctions. If any such...
``` update_abbrev : thm -> tactic ``` takes a theorem of the form `v = t` (and maybe also `t = v`), finds an `Abbrev` of the form `Abbrev(v =...
Currently rename will abbreviate in lossy fashion such that ``` rename [‘SUC n’] ``` when applied to a goal with conclusion ``` SUC (2 + x * y + z)...
This leads to very strange errors on case-insensitive file systems. Also arises if a theory is referenced in one place with one capitalisation and in another with a different one.
*Viz:* > SIMP_CONV (srw_ss() ++ numSimps.ARITH_ss) [] ``n2 + (fxx - 1) + 1 - n2``; Exception- UNCHANGED raised The `n2`'s should be cancelled even though the `-1` can't be...
As per [GNU make's facility](https://www.gnu.org/software/make/manual/html_node/Include.html). The ability to go back and attempt to build include files that are not found might be an optional part of this feature. Currently, I'm...
The references hidden inside compsets make manipulating them a pain. They also make concurrent operation hard.
Chained updates look bad: ``` (k1 =+ v1) ((k2 =+ v2) f) ``` or ``` f |+ (k1,v1) |+ (k2,v2) ``` Recent p/printing hacking for a paper suggests that these...
As per the [GNU make specification](https://www.gnu.org/software/make/manual/html_node/Make-Control-Functions.html) if possible.
For backwards compatibility, there could be a theory-level command that turned this back off again, but I think monadsyntax should be available by default, perhaps binding to the `option` monad....