wenzelm [Fri, 16 Mar 2012 21:59:19 +0100] rev 47842
afford strict Args.type_name (cf. 29e88714ffe4);
wenzelm [Fri, 16 Mar 2012 21:40:21 +0100] rev 47841
check declared vs. defined commands at end of session;
wenzelm [Fri, 16 Mar 2012 21:20:23 +0100] rev 47840
more abstract heading level;
wenzelm [Fri, 16 Mar 2012 20:45:47 +0100] rev 47839
less redundant data;
wenzelm [Fri, 16 Mar 2012 20:33:33 +0100] rev 47838
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
discontinued obsolete Keyword.thy_switch;
wenzelm [Fri, 16 Mar 2012 18:21:22 +0100] rev 47837
merged
wenzelm [Fri, 16 Mar 2012 18:20:12 +0100] rev 47836
outer syntax command definitions based on formal command_spec derived from theory header declarations;
paulson [Fri, 16 Mar 2012 16:32:34 +0000] rev 47835
ZF news
paulson [Fri, 16 Mar 2012 16:29:51 +0000] rev 47834
merged
paulson [Fri, 16 Mar 2012 16:29:28 +0000] rev 47833
Structured transfinite induction proofs