2000-12-13 nipkow [Wed, 13 Dec 2000 09:39:53 +0100] rev 10654
*** empty log message ***
doc-src/TutorialI/Advanced/Partial.thy doc-src/TutorialI/Advanced/ROOT.ML doc-src/TutorialI/Advanced/WFrec.thy doc-src/TutorialI/Advanced/advanced.tex doc-src/TutorialI/Advanced/document/Partial.tex doc-src/TutorialI/Advanced/document/WFrec.tex doc-src/TutorialI/CTL/CTL.thy doc-src/TutorialI/CTL/document/CTL.tex doc-src/TutorialI/Inductive/Even.tex doc-src/TutorialI/IsaMakefile doc-src/TutorialI/Misc/AdvancedInd.thy doc-src/TutorialI/Misc/document/natsum.tex doc-src/TutorialI/Misc/natsum.thy doc-src/TutorialI/Misc/simp.thy doc-src/TutorialI/Recdef/Nested2.thy doc-src/TutorialI/Recdef/document/Nested2.tex doc-src/TutorialI/Recdef/document/examples.tex doc-src/TutorialI/Recdef/document/termination.tex doc-src/TutorialI/Recdef/examples.thy doc-src/TutorialI/Recdef/termination.thy doc-src/TutorialI/ToyList/ToyList.thy doc-src/TutorialI/ToyList/document/ToyList.tex doc-src/TutorialI/Types/Axioms.thy doc-src/TutorialI/Types/Overloading2.thy doc-src/TutorialI/Types/Pairs.thy doc-src/TutorialI/Types/Typedef.thy doc-src/TutorialI/Types/document/Axioms.tex doc-src/TutorialI/Types/document/Overloading2.tex doc-src/TutorialI/Types/document/Pairs.tex doc-src/TutorialI/Types/document/Typedef.tex doc-src/TutorialI/Types/numerics.tex doc-src/TutorialI/appendix.tex doc-src/TutorialI/fp.tex doc-src/TutorialI/todo.tobias doc-src/TutorialI/tutorial.tex

2000-12-13 nipkow [Wed, 13 Dec 2000 09:32:55 +0100] rev 10653
small mods.
src/HOL/BCV/Kildall.ML src/HOL/Lambda/ListBeta.thy src/HOL/Library/While_Combinator.thy src/HOL/Library/While_Combinator_Example.thy src/HOL/Recdef.thy src/HOL/Wellfounded_Relations.ML

2000-12-13 nipkow [Wed, 13 Dec 2000 09:30:59 +0100] rev 10652
sar split method uses new gen_split_tac.
src/Provers/splitter.ML

2000-12-12 kleing [Tue, 12 Dec 2000 14:08:48 +0100] rev 10651
completeness (unfinished)
src/HOL/MicroJava/BV/JVM.thy

2000-12-12 kleing [Tue, 12 Dec 2000 14:08:26 +0100] rev 10650
added direction dynamic ==> static
src/HOL/MicroJava/BV/DFA_err.thy

2000-12-12 kleing [Tue, 12 Dec 2000 14:07:11 +0100] rev 10649
eliminated some warnings, tuned
src/HOL/MicroJava/BV/StepMono.thy

2000-12-12 paulson [Tue, 12 Dec 2000 12:01:19 +0100] rev 10648
first stage in tidying up Real and Hyperreal.
Factor cancellation simprocs
inverse #0 = #0
simprules for division
corrected ambigous syntax definitions in Hyperreal
src/HOL/Real/Hyperreal/HyperDef.ML src/HOL/Real/Hyperreal/Lim.ML src/HOL/Real/Hyperreal/Lim.thy src/HOL/Real/Hyperreal/NSA.ML src/HOL/Real/Hyperreal/SEQ.ML src/HOL/Real/Hyperreal/SEQ.thy src/HOL/Real/RealAbs.ML src/HOL/Real/RealArith.ML src/HOL/Real/RealBin.ML src/HOL/Real/RealDef.ML src/HOL/Real/RealDef.thy src/HOL/Real/RealOrd.ML src/HOL/Real/RealPow.ML

2000-12-12 paulson [Tue, 12 Dec 2000 11:59:25 +0100] rev 10647
deleting unused rules
src/HOL/Integ/IntDef.ML

2000-12-12 paulson [Tue, 12 Dec 2000 11:58:44 +0100] rev 10646
greater use of overloaded rules (order_less_imp_le not zless_imp_zle, ...)
src/HOL/Integ/Int.ML src/HOL/Integ/IntArith.ML

2000-12-12 paulson [Tue, 12 Dec 2000 11:57:33 +0100] rev 10645
auto-updated
doc-src/TutorialI/Advanced/document/simp.tex doc-src/TutorialI/CTL/document/CTL.tex doc-src/TutorialI/CTL/document/CTLind.tex doc-src/TutorialI/CTL/document/PDL.tex doc-src/TutorialI/Inductive/document/AB.tex doc-src/TutorialI/Inductive/document/Advanced.tex doc-src/TutorialI/Inductive/document/Even.tex doc-src/TutorialI/Inductive/document/Star.tex doc-src/TutorialI/Misc/document/AdvancedInd.tex doc-src/TutorialI/Misc/document/simp.tex doc-src/TutorialI/Recdef/document/Nested2.tex doc-src/TutorialI/Types/document/Axioms.tex doc-src/TutorialI/Types/document/Numbers.tex doc-src/TutorialI/Types/document/Typedef.tex