| Thu, 30 Aug 2012 09:47:46 +0200 | blanchet | started work on datatype sugar | changeset | files |
| Thu, 30 Aug 2012 09:47:46 +0200 | blanchet | killed obsolete "bnf_of_typ" command | changeset | files |
| Thu, 30 Aug 2012 09:47:46 +0200 | blanchet | removed dead code | changeset | files |
| Thu, 30 Aug 2012 09:47:46 +0200 | blanchet | have "bnf_of_typ" command seal the BNF | changeset | files |
| Thu, 30 Aug 2012 21:50:49 +0200 | wenzelm | register proofs of Isar goals, to enable recovery from unstable command states after interactive cancellation; | changeset | files |
| Thu, 30 Aug 2012 21:23:04 +0200 | wenzelm | refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390); | changeset | files |
| Thu, 30 Aug 2012 19:18:49 +0200 | wenzelm | some support for registering forked proofs within Proof.state, using its bottom context; | changeset | files |