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
huffman [Fri, 16 Mar 2012 15:51:53 +0100] rev 47832
make more word theorems respect int/bin distinction
wenzelm [Fri, 16 Mar 2012 14:46:13 +0100] rev 47831
refute_params are given in *this* theory;