HOL
HOL copied to clipboard
HOL-Theorem-Prover
Canonical sources for HOL4 theorem-proving system. Branch develop is where “mainline development” occurs; when develop passes our regression tests, master is merged forward to catch up.
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 >...
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...
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...
Isabelle's datatype package introduces a bunch of helpful constants on datatype definitions, see 2.1.5 Auxiliary Constants http://isabelle.in.tum.de/dist/Isabelle2020/doc/datatypes.pdf (thanks to @IlmariReissumies for the link) These seem like they could be nice...
Add syntax so that: ``` val frac_tyax = new_type_definition( "frac", Q.prove(`?x. (\f:int#int. 0i
``` 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)...
`EVERY2` and `LIST_REL` are the same constant (one is an overload for the other). But several theorems use "EVERY2" in their name, which makes it hard to find theorems about...
Consider the following Holmake invocation: ``` > Holmake -k Working in $(HOLDIR)/examples/balanced_bst [...] Working in . Holdep failed: tinyMachineScript.sml 469.66 Unescaped newline in string literal Holmake failed with exception: HolDepFailed...
The various tacticals (`THEN`, `THENL`, `THEN1`) could be made to parallelise evaluation of the tactics on multiple subgoals. (I think it's reasonable to treat tactics that aren't robust to such...
Metadata
Owner
Metadata
Canonical sources for HOL4 theorem-proving system. Branch develop is where “mainline development” occurs; when develop passes our regression tests, master is merged forward to catch up.