Wed, 31 Mar 2004 11:02:00 +0200 Lex now in AFP
nipkow [Wed, 31 Mar 2004 11:02:00 +0200] rev 14502
Lex now in AFP
Wed, 31 Mar 2004 11:00:25 +0200 HOL/Lex is now in AFP/Functional-Automata
nipkow [Wed, 31 Mar 2004 11:00:25 +0200] rev 14501
HOL/Lex is now in AFP/Functional-Automata
Wed, 31 Mar 2004 10:51:50 +0200 new
streckem [Wed, 31 Mar 2004 10:51:50 +0200] rev 14500
new
Tue, 30 Mar 2004 19:33:57 +0200 new
streckem [Tue, 30 Mar 2004 19:33:57 +0200] rev 14499
new
Tue, 30 Mar 2004 19:28:27 +0200 Added PSV 2003/2004
streckem [Tue, 30 Mar 2004 19:28:27 +0200] rev 14498
Added PSV 2003/2004
Tue, 30 Mar 2004 11:25:14 +0200 tidied
paulson [Tue, 30 Mar 2004 11:25:14 +0200] rev 14497
tidied
Tue, 30 Mar 2004 11:18:12 +0200 tidied
paulson [Tue, 30 Mar 2004 11:18:12 +0200] rev 14496
tidied
Tue, 30 Mar 2004 08:45:39 +0200 Added append_eq_append_conv2
nipkow [Tue, 30 Mar 2004 08:45:39 +0200] rev 14495
Added append_eq_append_conv2
Mon, 29 Mar 2004 15:35:04 +0200 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg [Mon, 29 Mar 2004 15:35:04 +0200] rev 14494
Added bitvector library (Word) to HOL/Library and a theory using it (Adder) to HOL/ex.
Mon, 29 Mar 2004 10:17:35 +0200 include exercises again
kleing [Mon, 29 Mar 2004 10:17:35 +0200] rev 14493
include exercises again
Mon, 29 Mar 2004 08:59:58 +0200 removed intro to isabelle
kleing [Mon, 29 Mar 2004 08:59:58 +0200] rev 14492
removed intro to isabelle
Mon, 29 Mar 2004 08:59:23 +0200 put in sections, reorganized, removed intro to isabelle
kleing [Mon, 29 Mar 2004 08:59:23 +0200] rev 14491
put in sections, reorganized, removed intro to isabelle
Mon, 29 Mar 2004 08:54:26 +0200 allow sections in contents file
kleing [Mon, 29 Mar 2004 08:54:26 +0200] rev 14490
allow sections in contents file
Fri, 26 Mar 2004 19:58:43 +0100 satsolver=dpll
webertj [Fri, 26 Mar 2004 19:58:43 +0100] rev 14489
satsolver=dpll
Fri, 26 Mar 2004 14:53:17 +0100 slightly different SAT solver interface
webertj [Fri, 26 Mar 2004 14:53:17 +0100] rev 14488
slightly different SAT solver interface
Fri, 26 Mar 2004 12:21:50 +0100 Installed solvers now determined at call time (as opposed to compile time)
webertj [Fri, 26 Mar 2004 12:21:50 +0100] rev 14487
Installed solvers now determined at call time (as opposed to compile time)
Fri, 26 Mar 2004 05:32:00 +0100 symbols in idents
kleing [Fri, 26 Mar 2004 05:32:00 +0100] rev 14486
symbols in idents
Thu, 25 Mar 2004 10:32:21 +0100 new material from Avigad
paulson [Thu, 25 Mar 2004 10:32:21 +0100] rev 14485
new material from Avigad
Thu, 25 Mar 2004 10:31:25 +0100 new treatment of equivalence classes
paulson [Thu, 25 Mar 2004 10:31:25 +0100] rev 14484
new treatment of equivalence classes
Thu, 25 Mar 2004 06:44:39 +0100 documented new identifier syntax
kleing [Thu, 25 Mar 2004 06:44:39 +0100] rev 14483
documented new identifier syntax
Thu, 25 Mar 2004 05:37:32 +0100 moved MiniML and AVL to archive of formal proofs
kleing [Thu, 25 Mar 2004 05:37:32 +0100] rev 14482
moved MiniML and AVL to archive of formal proofs
Wed, 24 Mar 2004 10:55:38 +0100 auto update
paulson [Wed, 24 Mar 2004 10:55:38 +0100] rev 14481
auto update
Wed, 24 Mar 2004 10:55:20 +0100 clarified
paulson [Wed, 24 Mar 2004 10:55:20 +0100] rev 14480
clarified
Wed, 24 Mar 2004 10:50:29 +0100 streamlined treatment of quotients for the integers
paulson [Wed, 24 Mar 2004 10:50:29 +0100] rev 14479
streamlined treatment of quotients for the integers
Fri, 19 Mar 2004 11:06:53 +0100 added a few 0 and Suc lemmas
nipkow [Fri, 19 Mar 2004 11:06:53 +0100] rev 14478
added a few 0 and Suc lemmas
Fri, 19 Mar 2004 10:51:03 +0100 conversion of Hyperreal/Lim to new-style
paulson [Fri, 19 Mar 2004 10:51:03 +0100] rev 14477
conversion of Hyperreal/Lim to new-style
Fri, 19 Mar 2004 10:50:06 +0100 removed redundant thms
paulson [Fri, 19 Mar 2004 10:50:06 +0100] rev 14476
removed redundant thms
Fri, 19 Mar 2004 10:48:22 +0100 new thms
paulson [Fri, 19 Mar 2004 10:48:22 +0100] rev 14475
new thms
Fri, 19 Mar 2004 10:46:25 +0100 New simplification ordering to move numerals together. Fixes a bug in the
paulson [Fri, 19 Mar 2004 10:46:25 +0100] rev 14474
New simplification ordering to move numerals together. Fixes a bug in the nat cancellation simprocs
Fri, 19 Mar 2004 10:44:20 +0100 stylistic tweaks
paulson [Fri, 19 Mar 2004 10:44:20 +0100] rev 14473
stylistic tweaks
(0) -10000 -3000 -1000 -300 -100 -50 -30 +30 +50 +100 +300 +1000 +3000 +10000 +30000 tip