2001-12-10 berghofe [Mon, 10 Dec 2001 15:16:49 +0100] rev 12436
Replaced several occurrences of "blast" by "rules".
src/HOL/HOL.thy

2001-12-10 wenzelm [Mon, 10 Dec 2001 13:30:14 +0100] rev 12435
document root;
src/FOL/ex/document/root.tex

2001-12-09 kleing [Sun, 09 Dec 2001 15:26:13 +0100] rev 12434
tuned
src/HOL/IMP/Denotation.thy src/HOL/IMP/Hoare.thy src/HOL/IMP/Transition.thy src/HOL/IMP/VC.thy

2001-12-09 kleing [Sun, 09 Dec 2001 14:37:42 +0100] rev 12433
HOLCF/IMP converted to Isar
src/HOLCF/IsaMakefile

2001-12-09 kleing [Sun, 09 Dec 2001 14:36:14 +0100] rev 12432
HOL/IMP converted to Isar
src/HOL/IsaMakefile

2001-12-09 kleing [Sun, 09 Dec 2001 14:35:36 +0100] rev 12431
converted to Isar
src/HOL/IMP/Com.thy src/HOL/IMP/Denotation.ML src/HOL/IMP/Denotation.thy src/HOL/IMP/Examples.ML src/HOL/IMP/Examples.thy src/HOL/IMP/Expr.ML src/HOL/IMP/Expr.thy src/HOL/IMP/Hoare.ML src/HOL/IMP/Hoare.thy src/HOL/IMP/Natural.ML src/HOL/IMP/Natural.thy src/HOL/IMP/Transition.ML src/HOL/IMP/Transition.thy src/HOL/IMP/VC.ML src/HOL/IMP/VC.thy src/HOLCF/IMP/Denotational.ML src/HOLCF/IMP/Denotational.thy src/HOLCF/IMP/HoareEx.ML src/HOLCF/IMP/HoareEx.thy

2001-12-09 kleing [Sun, 09 Dec 2001 14:35:11 +0100] rev 12430
latex output setup
src/HOL/IMP/document/root.bib src/HOL/IMP/document/root.tex src/HOLCF/IMP/document/root.bib src/HOLCF/IMP/document/root.tex

2001-12-09 kleing [Sun, 09 Dec 2001 14:34:56 +0100] rev 12429
tuned for latex output
src/HOL/IMP/Compiler.thy

2001-12-09 kleing [Sun, 09 Dec 2001 14:34:18 +0100] rev 12428
setup [trans] rules for calculational Isar reasoning
src/HOL/Transitive_Closure.thy

2001-12-08 wenzelm [Sat, 08 Dec 2001 17:34:46 +0100] rev 12427
use /var/tmp (which happens to be more spacious on atbroy37);
Admin/makebin