2006-06-07 wenzelm [Wed, 07 Jun 2006 02:01:32 +0200] rev 19809
added 'if' and 'for' keywords;
tuned;
src/Pure/Isar/isar_syn.ML

2006-06-07 wenzelm [Wed, 07 Jun 2006 02:01:31 +0200] rev 19808
added facts_of;
tuned interfaces;
src/Pure/Isar/element.ML

2006-06-07 wenzelm [Wed, 07 Jun 2006 02:01:30 +0200] rev 19807
added Tools/invoke.ML;
src/Pure/IsaMakefile

2006-06-07 wenzelm [Wed, 07 Jun 2006 02:01:28 +0200] rev 19806
renamed Type.(un)varifyT to Logic.(un)varifyT;
made (un)varify strict wrt. global context -- may use legacy_(un)varify as workaround;
src/HOL/Library/word_setup.ML src/HOL/Tools/datatype_realizer.ML src/HOL/Tools/function_package/termination.ML src/HOL/Tools/inductive_realizer.ML src/Pure/IsaPlanner/term_lib.ML src/Pure/Tools/class_package.ML src/Pure/Tools/codegen_package.ML src/Pure/Tools/codegen_theorems.ML src/Pure/codegen.ML src/Pure/defs.ML src/Pure/display.ML src/Pure/logic.ML src/Pure/sign.ML src/Pure/theory.ML src/Pure/type.ML

2006-06-07 wenzelm [Wed, 07 Jun 2006 02:01:27 +0200] rev 19805
do not open Logic;
src/FOLP/simp.ML

2006-06-07 wenzelm [Wed, 07 Jun 2006 01:59:17 +0200] rev 19804
tuned;
src/HOLCF/IOA/meta_theory/Seq.thy

2006-06-07 wenzelm [Wed, 07 Jun 2006 01:51:22 +0200] rev 19803
removed obsolete ML files;
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.ML src/HOL/IMPP/Misc.thy src/HOL/IMPP/Natural.ML src/HOL/IMPP/Natural.thy src/HOL/IsaMakefile

2006-06-07 wenzelm [Wed, 07 Jun 2006 01:06:53 +0200] rev 19802
removed obsolete ML files;
src/HOL/Hoare/Arith2.ML src/HOL/Hoare/Arith2.thy src/HOL/IsaMakefile

2006-06-07 wenzelm [Wed, 07 Jun 2006 00:57:14 +0200] rev 19801
removed obsolete ML files;
src/HOL/IOA/Asig.ML src/HOL/IOA/Asig.thy src/HOL/IOA/IOA.ML src/HOL/IOA/IOA.thy src/HOL/IOA/Solve.ML src/HOL/IOA/Solve.thy src/HOL/IsaMakefile

2006-06-06 wenzelm [Tue, 06 Jun 2006 20:47:12 +0200] rev 19800
removed Toplevel.debug;
src/Pure/Pure.thy