Michael Norrish

HOL_ERR to pick up term and type arguments

12

Change the fundamental exception to give exception-raisers the option of attaching relevant terms and types. For the sake of backwards compatibility, we can redefine helpers like `mk_HOL_ERR` and friends (creating...

Arithmetic normalisation of subtraction + SUC doesn't

1

If `0 < x` is in the assumptions `simp[]` still won't prove `f (SUC (x-1)) = f x`

Pattern-matching compilation fails

1

With the "classic" heuristic, this works. Now, with the new default, it fails (with an exception about missing cases): ``` val foo_def = Define` (foo 0 0 0 = 0)...

Rational number arithmetic (operations and comparisons) doesn’t EVAL

4

This is disgusting: ``` > EVAL ``3/4

Holmake should prioritise targets with many dependencies

4

When building things in parallel, things that have many dependencies should be preferred over targets that have fewer. E.g., in the extreme a long-running set of targets with no children...

At the moment, this tactic reveals the underlying use of a constructor, one that should be generally hidden.

In particular, given a definition such as ``` Datatype: rcd =

The `.HOLMK/lastmaker` file is created so Holmake (and the emacs mode) can tell which executables to use (useful on machines where multiple HOL installations are present). At the moment, this...

From the Isabelle mailing list (at https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2021-February/msg00034.html) > there is a Haskell extension that allows writing nested ifs in the following nice syntax: > if | P -> a >...

Alternative choices of induction theorem

8

Being able to write things like ``Induct_on `FINITE` `` is nice, but it'd be even nicer if one had a way of occasionally specifying different theorems from the default. (This...