New rewrite for isPrefix; make this and others automatic.
Prove the interesting PEG theorems.

Importantly, that well-formed grammars (those without left recursion)
always terminate on input strings (either rejecting or accepting
them).
Tidy parsing/pegScript, including: export totality theorem
SML code to act as inspiration for executable (in HOL) PEG parsing.
minor tweaks on quantHeuristicsLib, adept Holfoot to changes with MEM
Test and fix for omissions in computeLib’s handling of sums.
First attempt at executable CPS-style version of peg-parsing.

Doesn’t EVAL properly yet (it’s unclear to me if this is a problem
with EVAL or my definition).
Customise time format in Lib.time.

Gives more precision when < 1s and prints days/hours/minutes when appropriate.
Move (now working) PEG example into separate theory file.
Unwind (and hide) pegexec’s WHILE-loop to get two tail-recursive functions.
fix a bug in Vimhol tactic expansion

If the visually selected tactic was indented and folding was on, the
call sent to HOL was empty. New version of HOLExpand() that is maybe
simpler (because that's where I thought the problem was originally), and
new version of HOLCStart() turns off folding in the temporary buffer.
New (longer) example in pegSampleTheory.
Remove unnecessary listeval and LV constructor in executable PEG.

A tiny amount of partial evaluation completely eliminates the need for
these.
Define a pegparse constant that (provably) implements the peg_eval relation.

This is the natural entry-point for all executable parsing.

Still need to prove a nice executable version of the wfG constant that
checks whether or not a grammar is well-formed.
Hide (in the parsing sense) the internal PEG constants AP and EV.
Rename pegexec$eval to peg_exec to avoid grabbing name “eval”.
Minor wording improvement in the release notes about case-const-arg-flip.
Remove trailing whitespace in src/
Progress towards showing the connection between ACL2 and HOL ordinals.

In particular, show that the ord_less from ordinalNotation is the same
as < on the “real” ordinals.
A new keybinding for less-than-or-equals in hol-unicode.

C-Q is not great, but the mnemonic is ‘less than or eQuals’.