2001-12-14 wenzelm [Fri, 14 Dec 2001 11:51:01 +0100] rev 12495
export add_tvarsT etc.;
src/Pure/drule.ML

2001-12-14 wenzelm [Fri, 14 Dec 2001 11:50:38 +0100] rev 12494
changed Type.varify;
src/HOL/Tools/inductive_package.ML

2001-12-14 wenzelm [Fri, 14 Dec 2001 11:50:19 +0100] rev 12493
Term.invent_type_names;
src/Pure/axclass.ML

2001-12-13 nipkow [Thu, 13 Dec 2001 19:05:10 +0100] rev 12492
*** empty log message ***
doc-src/TutorialI/CTL/CTLind.thy doc-src/TutorialI/CTL/document/CTLind.tex doc-src/TutorialI/Misc/AdvancedInd.thy doc-src/TutorialI/Misc/document/AdvancedInd.tex doc-src/TutorialI/isabellesym.sty doc-src/TutorialI/todo.tobias

2001-12-13 nipkow [Thu, 13 Dec 2001 17:57:55 +0100] rev 12491
*** empty log message ***
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

2001-12-13 wenzelm [Thu, 13 Dec 2001 17:44:56 +0100] rev 12490
made SML/XL happy;
src/Pure/codegen.ML

2001-12-13 nipkow [Thu, 13 Dec 2001 16:48:34 +0100] rev 12489
*** empty log message ***
NEWS doc-src/TutorialI/CTL/CTL.thy doc-src/TutorialI/CTL/document/CTL.tex doc-src/TutorialI/Misc/document/simp.tex doc-src/TutorialI/Misc/simp.thy doc-src/TutorialI/Recdef/document/termination.tex doc-src/TutorialI/Recdef/termination.thy doc-src/TutorialI/Sets/Relations.thy doc-src/TutorialI/Sets/sets.tex doc-src/TutorialI/appendix.tex doc-src/TutorialI/preface.tex doc-src/TutorialI/todo.tobias doc-src/TutorialI/tutorial.tex

2001-12-13 nipkow [Thu, 13 Dec 2001 16:48:07 +0100] rev 12488
Terminator now uses arith_tac as well.
TFL/post.ML

2001-12-13 nipkow [Thu, 13 Dec 2001 16:47:35 +0100] rev 12487
comp -> rel_comp
src/HOL/Lex/RegExp2NA.ML src/HOL/Lex/RegExp2NAe.ML src/HOL/Relation.ML src/HOL/Relation.thy src/HOL/Relation_Power.ML src/HOL/Transitive_Closure_lemmas.ML

2001-12-13 wenzelm [Thu, 13 Dec 2001 15:45:03 +0100] rev 12486
isatool expandshort;
src/HOL/Algebra/poly/Degree.ML src/HOL/Hoare/Examples.ML src/HOL/Hyperreal/EvenOdd.ML src/HOL/Hyperreal/ExtraThms2.ML src/HOL/Hyperreal/Lim.ML src/HOL/Hyperreal/MacLaurin.ML src/HOL/Hyperreal/NSA.ML src/HOL/Hyperreal/NatStar.ML src/HOL/Hyperreal/NthRoot.ML src/HOL/Hyperreal/SEQ.ML src/HOL/Hyperreal/Series.ML src/HOL/Hyperreal/Star.ML src/HOL/Hyperreal/Transcendental.ML src/HOL/IMPP/Hoare.ML src/HOL/Induct/Com.ML src/HOL/Induct/SList.ML src/HOL/Integ/Bin.ML src/HOL/Integ/IntArith.ML src/HOL/Integ/NatSimprocs.ML src/HOL/Integ/int_arith2.ML src/HOL/Lex/AutoChopper.ML src/HOL/List.ML src/HOL/Nat.ML src/HOL/Prolog/Func.ML src/HOL/Prolog/Test.ML src/HOL/Prolog/Type.ML src/HOL/Transitive_Closure_lemmas.ML src/HOL/Wellfounded_Recursion.ML src/HOL/Wellfounded_Relations.ML src/HOL/equalities.ML src/HOL/ex/AVL.ML src/HOL/ex/Puzzle.ML src/HOL/ex/Sorting.ML