2000-10-17 nipkow [Tue, 17 Oct 2000 13:28:57 +0200] rev 10236
*** empty log message ***
doc-src/TutorialI/Inductive/AB.thy doc-src/TutorialI/Inductive/document/AB.tex doc-src/TutorialI/Misc/AdvancedInd.thy doc-src/TutorialI/Misc/document/AdvancedInd.tex doc-src/TutorialI/ToyList/ToyList.thy doc-src/TutorialI/ToyList/document/ToyList.tex doc-src/TutorialI/todo.tobias doc-src/TutorialI/tutorial.tex

2000-10-17 paulson [Tue, 17 Oct 2000 10:45:51 +0200] rev 10235
renaming of contrapos rules
doc-src/TutorialI/CTL/CTL.thy doc-src/TutorialI/CTL/CTLind.thy

2000-10-17 paulson [Tue, 17 Oct 2000 10:27:28 +0200] rev 10234
tidied some awkward proofs
src/HOL/equalities.ML

2000-10-17 paulson [Tue, 17 Oct 2000 10:26:07 +0200] rev 10233
tidying; removed unused rev_contra_subsetD
src/HOL/Set.ML

2000-10-17 paulson [Tue, 17 Oct 2000 10:23:16 +0200] rev 10232
restoration of "equalityI"; renaming of contrapos rules
src/HOL/Real/PRat.ML src/HOL/Real/PReal.ML src/HOL/Real/RealDef.ML

2000-10-17 paulson [Tue, 17 Oct 2000 10:21:12 +0200] rev 10231
renaming of contrapos rules
src/HOL/HOL_lemmas.ML src/HOL/Induct/Multiset.ML src/HOL/NatDef.ML src/HOL/Ord.ML src/HOL/Real/PNat.ML src/HOL/TLA/Memory/Memory.ML src/HOL/TLA/Memory/MemoryImplementation.ML src/HOL/TLA/TLA.ML src/HOL/Wellfounded_Relations.ML src/HOL/cladata.ML src/HOL/simpdata.ML

2000-10-17 paulson [Tue, 17 Oct 2000 10:20:43 +0200] rev 10230
tidying and renaming of contrapos rules
src/HOL/Algebra/abstract/Ideal.ML src/HOL/Algebra/abstract/Ring.ML src/HOL/Algebra/poly/Degree.ML src/HOL/Algebra/poly/PolyRing.ML src/HOL/Real/Hyperreal/NSA.ML src/HOLCF/Cfun3.ML src/HOLCF/Fix.ML src/HOLCF/IOA/meta_theory/CompoTraces.ML src/HOLCF/Sprod0.ML src/HOLCF/Sprod3.ML src/HOLCF/Ssum0.ML src/HOLCF/Ssum3.ML src/HOLCF/Up3.ML src/HOLCF/domain/theorems.ML src/HOLCF/ex/Stream.ML

2000-10-17 oheimb [Tue, 17 Oct 2000 08:41:42 +0200] rev 10229
cosmetics
src/HOL/MicroJava/J/Example.thy

2000-10-17 nipkow [Tue, 17 Oct 2000 08:00:46 +0200] rev 10228
added intermediate value thms
src/HOL/Integ/IntArith.ML

2000-10-17 nipkow [Tue, 17 Oct 2000 08:00:34 +0200] rev 10227
<= -> \<le>
src/HOL/Ord.thy