2000-09-12 wenzelm [Tue, 12 Sep 2000 22:13:23 +0200] rev 9941
renamed atts: rulify to rule_format, elimify to elim_format;
NEWS doc-src/IsarRef/generic.tex doc-src/IsarRef/hol.tex doc-src/IsarRef/refcard.tex doc-src/TutorialI/Misc/AdvancedInd.thy src/HOL/Induct/Acc.thy src/HOL/Isar_examples/MutilatedCheckerboard.thy src/HOL/Isar_examples/Puzzle.thy src/HOL/Lambda/Eta.thy src/HOL/Lambda/InductTermi.thy src/HOL/Lambda/Lambda.thy src/HOL/Lambda/ListApplication.thy src/HOL/Lambda/ListBeta.thy src/HOL/Lambda/ListOrder.thy src/HOL/Lambda/ParRed.thy src/HOL/Lambda/Type.thy src/HOL/MicroJava/BV/BVSpecTypeSafe.thy src/HOL/MicroJava/BV/Convert.thy src/HOL/MicroJava/BV/Correct.thy src/HOL/MicroJava/BV/LBVComplete.thy src/HOL/MicroJava/BV/LBVCorrect.thy src/HOL/MicroJava/BV/StepMono.thy src/HOL/Real/HahnBanach/Aux.thy src/HOL/Real/HahnBanach/Subspace.thy src/HOL/ex/Primes.thy src/Provers/classical.ML src/Provers/rulify.ML src/Pure/Isar/attrib.ML

2000-09-12 nipkow [Tue, 12 Sep 2000 19:03:13 +0200] rev 9940
*** empty log message ***
doc-src/TutorialI/Recdef/Nested2.thy doc-src/TutorialI/Recdef/document/Nested2.tex

2000-09-12 wenzelm [Tue, 12 Sep 2000 17:39:29 +0200] rev 9939
tuned handling of "intros";
src/HOL/Tools/inductive_package.ML

2000-09-12 wenzelm [Tue, 12 Sep 2000 17:38:49 +0200] rev 9938
delrule: handle dest rules as well;
replaced "delrule" by "rule del";
src/Provers/classical.ML src/Pure/Isar/method.ML

2000-09-12 wenzelm [Tue, 12 Sep 2000 17:35:09 +0200] rev 9937
replaced "delrule" by "rule del";
NEWS

2000-09-12 wenzelm [Tue, 12 Sep 2000 17:34:50 +0200] rev 9936
renamed "delrule" to "rule del";
doc-src/IsarRef/generic.tex doc-src/IsarRef/pure.tex

2000-09-12 wenzelm [Tue, 12 Sep 2000 17:34:41 +0200] rev 9935
tuned;
doc-src/IsarRef/hol.tex

2000-09-12 wenzelm [Tue, 12 Sep 2000 17:01:14 +0200] rev 9934
tuned;
Admin/makedist Admin/page/dist-content/binary.content Admin/page/dist-content/docs.content Admin/page/dist-content/source.content

2000-09-12 nipkow [Tue, 12 Sep 2000 15:43:15 +0200] rev 9933
*** empty log message ***
doc-src/TutorialI/CodeGen/CodeGen.thy doc-src/TutorialI/Datatype/Fundata.thy doc-src/TutorialI/Datatype/Nested.thy doc-src/TutorialI/Datatype/document/Fundata.tex doc-src/TutorialI/Datatype/document/Nested.tex doc-src/TutorialI/Ifexpr/Ifexpr.thy doc-src/TutorialI/Ifexpr/document/Ifexpr.tex doc-src/TutorialI/IsaMakefile doc-src/TutorialI/Misc/AdvancedInd.thy doc-src/TutorialI/Misc/document/AdvancedInd.tex doc-src/TutorialI/Misc/document/pairs.tex doc-src/TutorialI/Misc/document/simp.tex doc-src/TutorialI/Misc/document/types.tex doc-src/TutorialI/Misc/pairs.thy doc-src/TutorialI/Misc/types.thy doc-src/TutorialI/Recdef/Nested1.thy doc-src/TutorialI/Recdef/Nested2.thy doc-src/TutorialI/Recdef/document/Nested1.tex doc-src/TutorialI/Recdef/document/Nested2.tex doc-src/TutorialI/Recdef/document/examples.tex doc-src/TutorialI/Recdef/document/simplification.tex doc-src/TutorialI/Recdef/document/termination.tex doc-src/TutorialI/Recdef/examples.thy doc-src/TutorialI/Recdef/simplification.thy doc-src/TutorialI/Recdef/termination.thy doc-src/TutorialI/Trie/Trie.thy doc-src/TutorialI/Trie/document/Trie.tex doc-src/TutorialI/appendix.tex doc-src/TutorialI/basics.tex doc-src/TutorialI/fp.tex doc-src/TutorialI/tricks.tex

2000-09-12 nipkow [Tue, 12 Sep 2000 14:59:44 +0200] rev 9932
*** empty log message ***
doc-src/TutorialI/Misc/simp.thy