Wed, 24 Feb 2010 14:20:07 -0800 change domain package's treatment of variable names in theorems to be like datatype package
huffman [Wed, 24 Feb 2010 14:20:07 -0800] rev 35443
change domain package's treatment of variable names in theorems to be like datatype package
Wed, 24 Feb 2010 14:13:15 -0800 remove redundant lemma real_minus_half_eq
huffman [Wed, 24 Feb 2010 14:13:15 -0800] rev 35442
remove redundant lemma real_minus_half_eq
Wed, 24 Feb 2010 10:36:17 -0800 polished and converted some proofs to Isar style
huffman [Wed, 24 Feb 2010 10:36:17 -0800] rev 35441
polished and converted some proofs to Isar style
Tue, 02 Mar 2010 12:26:50 +0100 killed more recdefs
krauss [Tue, 02 Mar 2010 12:26:50 +0100] rev 35440
killed more recdefs
Mon, 01 Mar 2010 18:49:55 +0100 tuned comment
krauss [Mon, 01 Mar 2010 18:49:55 +0100] rev 35439
tuned comment
Tue, 02 Mar 2010 09:05:50 +0100 repaired subscripts broken in d8d7d1b785af
haftmann [Tue, 02 Mar 2010 09:05:50 +0100] rev 35438
repaired subscripts broken in d8d7d1b785af
Tue, 02 Mar 2010 08:28:06 +0100 repaired definition (cf. d8d7d1b785af)
haftmann [Tue, 02 Mar 2010 08:28:06 +0100] rev 35437
repaired definition (cf. d8d7d1b785af)
Wed, 03 Mar 2010 15:40:39 +0100 authentic syntax for *all* logical entities;
wenzelm [Wed, 03 Mar 2010 15:40:39 +0100] rev 35436
authentic syntax for *all* logical entities;
Wed, 03 Mar 2010 12:03:47 +0100 mark_atoms: more precise treatment of SynExt.standard_token_markers vs. syntax consts;
wenzelm [Wed, 03 Mar 2010 12:03:47 +0100] rev 35435
mark_atoms: more precise treatment of SynExt.standard_token_markers vs. syntax consts;
Wed, 03 Mar 2010 12:02:59 +0100 notation for xsymbols (cf. ad039d29e01c);
wenzelm [Wed, 03 Mar 2010 12:02:59 +0100] rev 35434
notation for xsymbols (cf. ad039d29e01c);
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip