2001-07-25 paulson [Wed, 25 Jul 2001 13:33:08 +0200] rev 11452
removed reference to Ex_def
src/HOLCF/Porder.ML

2001-07-25 paulson [Wed, 25 Jul 2001 13:13:01 +0200] rev 11451
partial restructuring to reduce dependence on Axiom of Choice
src/HOL/Datatype_Universe.thy src/HOL/Finite.ML src/HOL/Finite.thy src/HOL/Fun.ML src/HOL/Fun.thy src/HOL/GroupTheory/Bij.thy src/HOL/GroupTheory/Ring.thy src/HOL/HOL.ML src/HOL/HOL.thy src/HOL/HOL_lemmas.ML src/HOL/Hilbert_Choice.thy src/HOL/Integ/Int.thy src/HOL/Integ/IntDef.thy src/HOL/IsaMakefile src/HOL/Nat.thy src/HOL/NatArith.ML src/HOL/Ord.thy src/HOL/Product_Type.thy src/HOL/Product_Type_lemmas.ML src/HOL/Relation.ML src/HOL/Wellfounded_Recursion.ML src/HOL/Wellfounded_Recursion.thy src/HOL/Wellfounded_Relations.thy src/HOL/cladata.ML src/HOL/ex/Tarski.ML src/HOL/ex/mesontest.ML src/HOL/ex/mesontest2.ML src/HOL/mono.ML src/HOL/simpdata.ML

2001-07-24 paulson [Tue, 24 Jul 2001 11:25:54 +0200] rev 11450
tweaks and indexing
doc-src/TutorialI/ToyList/ToyList.thy doc-src/TutorialI/ToyList/document/ToyList.tex doc-src/TutorialI/appendix.tex doc-src/TutorialI/basics.tex doc-src/TutorialI/fp.tex doc-src/TutorialI/preface.tex doc-src/TutorialI/tutorial.ind doc-src/TutorialI/tutorial.tex

2001-07-23 oheimb [Mon, 23 Jul 2001 19:06:11 +0200] rev 11449
cosmetics
src/HOL/NanoJava/AxSem.thy

2001-07-23 paulson [Mon, 23 Jul 2001 17:47:49 +0200] rev 11448
Final version of Florian Kammueller's examples
src/HOL/GroupTheory/Bij.ML src/HOL/GroupTheory/Bij.thy src/HOL/GroupTheory/FactGroup.ML src/HOL/GroupTheory/FactGroup.thy src/HOL/GroupTheory/Homomorphism.ML src/HOL/GroupTheory/Homomorphism.thy src/HOL/GroupTheory/Ring.ML src/HOL/GroupTheory/Ring.thy src/HOL/GroupTheory/RingConstr.ML src/HOL/GroupTheory/RingConstr.thy

2001-07-23 paulson [Mon, 23 Jul 2001 17:46:40 +0200] rev 11447
new GroupTheory examples; PiSets moved to GroupTheory, while LocaleGroup deleted
src/HOL/IsaMakefile

2001-07-23 paulson [Mon, 23 Jul 2001 17:45:54 +0200] rev 11446
improved version of the Pi-theorems
src/HOL/Fun.ML

2001-07-23 paulson [Mon, 23 Jul 2001 17:45:35 +0200] rev 11445
PiSets moved to GroupTheory, while LocaleGroup deleted
src/HOL/ex/LocaleGroup.ML src/HOL/ex/LocaleGroup.thy src/HOL/ex/PiSets.ML src/HOL/ex/PiSets.thy src/HOL/ex/ROOT.ML

2001-07-23 paulson [Mon, 23 Jul 2001 17:45:07 +0200] rev 11444
live links
src/HOL/ex/README.html

2001-07-23 paulson [Mon, 23 Jul 2001 17:37:29 +0200] rev 11443
The final version of Florian Kammueller's proofs
src/HOL/GroupTheory/Coset.ML src/HOL/GroupTheory/DirProd.ML src/HOL/GroupTheory/Group.ML src/HOL/GroupTheory/PiSets.ML src/HOL/GroupTheory/PiSets.thy src/HOL/GroupTheory/README.html src/HOL/GroupTheory/ROOT.ML src/HOL/GroupTheory/Sylow.ML src/HOL/GroupTheory/Sylow.thy