Michael Norrish

E.g., turn a theorem like 0 < x ** y .... into 1

As per this comment to `hol-info` by John Harrison: > HOL Light has a variant of the inductive relation command called "new_inductive_set" (written by Marco Maggesi) that lets you express...

Consider inverting sense of parenthesis-style directive ParoundPrec

2

Currently the documentation says: > The `ParoundPrec` value [...] causes parentheses to be added when the term is the argument to a function with a different precedence level. The code...

The normalisation process used in `ARITH` treats something like n = 10 \/ n = 9 \/ n = 8 ... \/ n = 0 extremely badly, creating a term...

Make Unwind work with some

1

There's a theorem roughly like ``` (some x. (x = v) /\ P(x)) = if P(v) then SOME v else NONE ``` that should be used in the simplifier's unwind...

Handle paired-abstractions better

4

In particular, if there is a quantifier over a variable of pair type, and that same variable is an argument to a paired abstraction, then the quantifier should be rewritten...

 As _per_ picture, we think we have a story for the creation and use of articles that assert axioms, constants and types, and then prove consequences thereof. We can...

The default behaviour of the simplifier (_i.e._, with `srw_ss()`) doesn't adjust the following: ``` f((x:int) - 2 + 1) ``` There doesn't seem much reason to leave terms like this...

E.g., ``` Datatype`foo = C | D num string | E foo num` ``` The machinery would have to define an auxiliary type, turning the above into ``` Datatype`foo =...