Fri, 16 Mar 2012 20:45:47 +0100 less redundant data;
wenzelm [Fri, 16 Mar 2012 20:45:47 +0100] rev 46968
less redundant data;
Fri, 16 Mar 2012 20:33:33 +0100 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm [Fri, 16 Mar 2012 20:33:33 +0100] rev 46967
uniform keyword names within ML/Scala -- produce elisp names via external conversion; discontinued obsolete Keyword.thy_switch;
Fri, 16 Mar 2012 18:21:22 +0100 merged
wenzelm [Fri, 16 Mar 2012 18:21:22 +0100] rev 46966
merged
Fri, 16 Mar 2012 16:32:34 +0000 ZF news
paulson [Fri, 16 Mar 2012 16:32:34 +0000] rev 46965
ZF news
Fri, 16 Mar 2012 16:29:51 +0000 merged
paulson [Fri, 16 Mar 2012 16:29:51 +0000] rev 46964
merged
Fri, 16 Mar 2012 16:29:28 +0000 Structured transfinite induction proofs
paulson [Fri, 16 Mar 2012 16:29:28 +0000] rev 46963
Structured transfinite induction proofs
Fri, 16 Mar 2012 15:51:53 +0100 make more word theorems respect int/bin distinction
huffman [Fri, 16 Mar 2012 15:51:53 +0100] rev 46962
make more word theorems respect int/bin distinction
Fri, 16 Mar 2012 18:20:12 +0100 outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm [Fri, 16 Mar 2012 18:20:12 +0100] rev 46961
outer syntax command definitions based on formal command_spec derived from theory header declarations;
Fri, 16 Mar 2012 14:46:13 +0100 refute_params are given in *this* theory;
wenzelm [Fri, 16 Mar 2012 14:46:13 +0100] rev 46960
refute_params are given in *this* theory;
Fri, 16 Mar 2012 14:42:11 +0100 defer actual parsing of command spans and thus allow new commands to be used in the same theory where defined;
wenzelm [Fri, 16 Mar 2012 14:42:11 +0100] rev 46959
defer actual parsing of command spans and thus allow new commands to be used in the same theory where defined;
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 tip