2002-01-16 wenzelm [Wed, 16 Jan 2002 20:58:27 +0100] rev 12779
export beta_eta_conversion;
src/Pure/meta_simplifier.ML

2002-01-16 wenzelm [Wed, 16 Jan 2002 20:57:02 +0100] rev 12778
Interface/proof_general.ML move to proof_general.ML;
src/Pure/Interface/ROOT.ML src/Pure/Interface/proof_general.ML src/Pure/IsaMakefile src/Pure/ROOT.ML src/Pure/proof_general.ML

2002-01-16 paulson [Wed, 16 Jan 2002 17:53:22 +0100] rev 12777
Isar version of ZF/AC
NEWS

2002-01-16 paulson [Wed, 16 Jan 2002 17:52:06 +0100] rev 12776
Isar version of AC
src/ZF/AC/AC15_WO6.ML src/ZF/AC/AC15_WO6.thy src/ZF/AC/AC16_WO4.ML src/ZF/AC/AC16_WO4.thy src/ZF/AC/AC16_lemmas.ML src/ZF/AC/AC16_lemmas.thy src/ZF/AC/AC17_AC1.ML src/ZF/AC/AC17_AC1.thy src/ZF/AC/AC18_AC19.ML src/ZF/AC/AC18_AC19.thy src/ZF/AC/AC1_WO2.ML src/ZF/AC/AC1_WO2.thy src/ZF/AC/AC7_AC9.ML src/ZF/AC/AC_Equiv.ML src/ZF/AC/AC_Equiv.thy src/ZF/AC/Cardinal_aux.ML src/ZF/AC/Cardinal_aux.thy src/ZF/AC/DC.ML src/ZF/AC/DC.thy src/ZF/AC/DC_lemmas.ML src/ZF/AC/DC_lemmas.thy src/ZF/AC/HH.ML src/ZF/AC/HH.thy src/ZF/AC/Hartog.ML src/ZF/AC/Hartog.thy src/ZF/AC/ROOT.ML src/ZF/AC/WO1_AC.ML src/ZF/AC/WO1_AC.thy src/ZF/AC/WO1_WO7.ML src/ZF/AC/WO1_WO7.thy src/ZF/AC/WO2_AC16.ML src/ZF/AC/WO2_AC16.thy src/ZF/AC/WO6_WO1.ML src/ZF/AC/WO6_WO1.thy src/ZF/AC/WO_AC.ML src/ZF/AC/WO_AC.thy src/ZF/AC/recfunAC16.ML src/ZF/AC/recfunAC16.thy src/ZF/AC/rel_is_fun.ML src/ZF/AC/rel_is_fun.thy src/ZF/CardinalArith.thy src/ZF/IsaMakefile src/ZF/Main.thy

2002-01-16 wenzelm [Wed, 16 Jan 2002 15:04:37 +0100] rev 12775
norm_hhf;
src/Pure/Isar/attrib.ML

2002-01-15 kleing [Tue, 15 Jan 2002 23:23:09 +0100] rev 12774
fixed theory deps
src/HOL/MicroJava/BV/Correct.thy

2002-01-15 kleing [Tue, 15 Jan 2002 22:22:05 +0100] rev 12773
use exec_lub instead of some_lub
src/HOL/MicroJava/BV/JType.thy src/HOL/MicroJava/BV/Semilat.thy src/HOL/MicroJava/ROOT.ML

2002-01-15 kleing [Tue, 15 Jan 2002 22:21:30 +0100] rev 12772
tuned for directly executable definitions
src/HOL/MicroJava/BV/Effect.thy

2002-01-15 wenzelm [Tue, 15 Jan 2002 21:09:31 +0100] rev 12771
tuned;
doc-src/TutorialI/Documents/Documents.thy doc-src/TutorialI/Documents/document/Documents.tex

2002-01-15 wenzelm [Tue, 15 Jan 2002 21:09:01 +0100] rev 12770
removed second copy of show_hyps;
src/Pure/Isar/proof_context.ML