Michael Norrish

Currently, the translator dumps all of its state to "disk" with every export theory, when really, it should just dump the changes (new stuff) to disk and then have the...

See motivation at: https://utcc.utoronto.ca/~cks/space/blog/sysadmin/ReportConfigFileLocations

Inductive definition should better diagnose syntax problems

3

Using a rule like `p ==> q ==> r` fails with very cryptic message, when it should diagnose that it actually just needs `p /\ q ==> r`.

emacs mode should choose HOL executable based on lastmaker file (if any)

1

See #1100 for inspiration.

The modern syntax could stash line-number information for theorems that could in turn be put into comments in the `xTheory.sig` file for possible reference by tools (or even dedicated humans)....

Consider use of Makarius' YXML library

4

See http://permalink.gmane.org/gmane.comp.mathematics.hol/1502 and https://bitbucket.org/makarius/yxml/src/ We already have a compressed (hash-consed) format for our types, terms and theorems in `DiskThms` and `TheoryPP`. ## Want to back this issue? **[Post a bounty...

Case expression prints badly

1

The definition ``` Definition a_def: a x = case x of | y::ys => if y = T then SOME y else SOME F | [] => NONE End ```...

Introducing an `Abbrev(newv = oldv)` assumption seems wasteful; should just rename (as _per_ that tactic) the occurrences of `oldv` into `newv`.

Amjad style lazy theorems

5

As per Hasan Amjad’s TPHOLs’05 paper. These could be used interactively at the level of calls to `prove` and `store_thm`, with worker thread(s) spawned to handle proofs in the background....

Induct_on / using example

2

``` Induct_on `RTC` using relationTheory.RTC_ALT_RIGHT_INDUCT ``` should work.