2005-09-18 wenzelm [Sun, 18 Sep 2005 15:20:08 +0200] rev 17481
converted to Isar theory format;
src/Sequents/ILL.ML src/Sequents/ILL.thy src/Sequents/ILL/ILL_predlog.ML src/Sequents/ILL/ILL_predlog.thy src/Sequents/ILL/ROOT.ML src/Sequents/ILL/washing.ML src/Sequents/ILL/washing.thy src/Sequents/LK.thy src/Sequents/LK/Nat.ML src/Sequents/LK/Nat.thy src/Sequents/LK/ROOT.ML src/Sequents/LK/hardquant.ML src/Sequents/LK/prop.ML src/Sequents/LK/quant.ML src/Sequents/LK0.ML src/Sequents/LK0.thy src/Sequents/Modal/ROOT.ML src/Sequents/Modal0.ML src/Sequents/Modal0.thy src/Sequents/ROOT.ML src/Sequents/S4.ML src/Sequents/S4.thy src/Sequents/S43.ML src/Sequents/S43.thy src/Sequents/Sequents.thy src/Sequents/T.ML src/Sequents/T.thy src/Sequents/simpdata.ML

2005-09-18 wenzelm [Sun, 18 Sep 2005 14:25:48 +0200] rev 17480
converted to Isar theory format;
src/FOLP/FOLP.ML src/FOLP/FOLP.thy src/FOLP/FOLP_lemmas.ML src/FOLP/IFOLP.ML src/FOLP/IFOLP.thy src/FOLP/IsaMakefile src/FOLP/ROOT.ML src/FOLP/ex/If.ML src/FOLP/ex/If.thy src/FOLP/ex/Nat.ML src/FOLP/ex/Nat.thy src/FOLP/ex/ROOT.ML src/FOLP/ex/cla.ML src/FOLP/ex/foundn.ML src/FOLP/ex/int.ML src/FOLP/ex/intro.ML src/FOLP/ex/prop.ML src/FOLP/ex/quant.ML src/FOLP/simpdata.ML

2005-09-17 wenzelm [Sat, 17 Sep 2005 20:49:14 +0200] rev 17479
converted to Isar theory format;
src/HOL/Algebra/abstract/Factor.ML src/HOL/Algebra/abstract/Factor.thy src/HOL/Algebra/abstract/Field.thy src/HOL/Algebra/abstract/Ideal.ML src/HOL/Algebra/abstract/Ideal.thy src/HOL/Algebra/abstract/PID.thy src/HOL/Algebra/abstract/RingHomo.ML src/HOL/Algebra/abstract/RingHomo.thy src/HOL/Algebra/poly/PolyHomo.ML src/HOL/Algebra/poly/PolyHomo.thy

2005-09-17 wenzelm [Sat, 17 Sep 2005 20:16:35 +0200] rev 17478
tuned;
TODO

2005-09-17 wenzelm [Sat, 17 Sep 2005 20:14:30 +0200] rev 17477
converted to Isar theory format;
src/HOL/IMPP/Com.ML src/HOL/IMPP/Com.thy src/HOL/IMPP/EvenOdd.ML src/HOL/IMPP/EvenOdd.thy src/HOL/IMPP/Hoare.ML src/HOL/IMPP/Hoare.thy src/HOL/IMPP/Misc.thy src/HOL/IMPP/Natural.ML src/HOL/IMPP/Natural.thy

2005-09-17 wenzelm [Sat, 17 Sep 2005 19:17:35 +0200] rev 17476
moved quick_and_dirty to Pure/ROOT.ML;
src/Pure/Isar/skip_proof.ML

2005-09-17 wenzelm [Sat, 17 Sep 2005 19:17:34 +0200] rev 17475
pretty_thm_aux: ora masked by quick_and_dirty;
src/Pure/display.ML

2005-09-17 wenzelm [Sat, 17 Sep 2005 19:17:33 +0200] rev 17474
added quick_and_dirty (from Isar/skip_proofs.ML);
src/Pure/ROOT.ML

2005-09-17 wenzelm [Sat, 17 Sep 2005 19:12:58 +0200] rev 17473
manually generated from Isabelle/HOLCF/IOA/Complex/Import;
etc/isar-keywords.el

2005-09-17 wenzelm [Sat, 17 Sep 2005 18:25:11 +0200] rev 17472
tuned document;
src/HOL/Datatype_Universe.thy src/HOL/Integ/IntArith.thy src/HOL/Integ/NatSimprocs.thy src/HOL/Integ/Parity.thy