blanchet [Thu, 30 Aug 2012 09:47:46 +0200] rev 49018
renamed ML function for consistency
blanchet [Thu, 30 Aug 2012 09:47:46 +0200] rev 49017
started work on datatype sugar
blanchet [Thu, 30 Aug 2012 09:47:46 +0200] rev 49016
killed obsolete "bnf_of_typ" command
blanchet [Thu, 30 Aug 2012 09:47:46 +0200] rev 49015
removed dead code
blanchet [Thu, 30 Aug 2012 09:47:46 +0200] rev 49014
have "bnf_of_typ" command seal the BNF
wenzelm [Thu, 30 Aug 2012 21:50:49 +0200] rev 49013
register proofs of Isar goals, to enable recovery from unstable command states after interactive cancellation;
wenzelm [Thu, 30 Aug 2012 21:23:04 +0200] rev 49012
refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390);
stretched meaning of Goal.parallel_proofs to enable future_terminal_proofs in interactive document model, despite its lack for regular forking of proofs;
wenzelm [Thu, 30 Aug 2012 19:18:49 +0200] rev 49011
some support for registering forked proofs within Proof.state, using its bottom context;
tuned signature;
wenzelm [Thu, 30 Aug 2012 16:39:50 +0200] rev 49010
tuned signature;
wenzelm [Thu, 30 Aug 2012 15:26:37 +0200] rev 49009
refined status of forked goals;