2000-08-28 wenzelm [Mon, 28 Aug 2000 13:52:38 +0200] rev 9695
proper setup of iman.sty/extra.sty/ttbox.sty;
doc-src/HOL/HOL.tex doc-src/HOL/Makefile doc-src/HOL/logics-HOL.tex doc-src/Inductive/Makefile doc-src/Inductive/ind-defs.tex doc-src/Intro/Makefile doc-src/Intro/advanced.tex doc-src/Intro/foundations.tex doc-src/Intro/getting.tex doc-src/Intro/intro.tex doc-src/IsarRef/Makefile doc-src/IsarRef/hol.tex doc-src/IsarRef/isar-ref.tex doc-src/IsarRef/pure.tex doc-src/IsarRef/refcard.tex doc-src/Logics/CTT.tex doc-src/Logics/LK.tex doc-src/Logics/Makefile doc-src/Logics/Old_HOL.tex doc-src/Logics/logics.tex doc-src/Logics/preface.tex doc-src/Logics/syntax.tex doc-src/Ref/Makefile doc-src/Ref/classical.tex doc-src/Ref/introduction.tex doc-src/Ref/ref.tex doc-src/Ref/simp.tex doc-src/Ref/simplifier.tex doc-src/Ref/substitution.tex doc-src/Ref/syntax.tex doc-src/Ref/tactic.tex doc-src/Ref/theories.tex doc-src/Ref/theory-syntax.tex doc-src/System/Makefile doc-src/System/fonts.tex doc-src/System/present.tex doc-src/System/system.tex doc-src/Tutorial/Makefile doc-src/Tutorial/extra.sty doc-src/Tutorial/ttbox.sty doc-src/Tutorial/tutorial.tex doc-src/TutorialI/Makefile doc-src/TutorialI/extra.sty doc-src/TutorialI/ttbox.sty doc-src/TutorialI/tutorial.tex doc-src/ZF/FOL.tex doc-src/ZF/Makefile doc-src/ZF/ZF.tex doc-src/ZF/logics-ZF.tex

2000-08-28 wenzelm [Mon, 28 Aug 2000 13:50:24 +0200] rev 9694
updated;
doc-src/AxClass/generated/isabelle.sty doc-src/AxClass/generated/isabellesym.sty

2000-08-28 wenzelm [Mon, 28 Aug 2000 13:48:47 +0200] rev 9693
moved \tt things to ttbox.sty;
removed \Pure etc;
doc-src/iman.sty

2000-08-28 wenzelm [Mon, 28 Aug 2000 13:48:25 +0200] rev 9692
proper setup;
doc-src/ttbox.sty

2000-08-28 wenzelm [Mon, 28 Aug 2000 13:48:14 +0200] rev 9691
removed ttbox;
doc-src/extra.sty

2000-08-28 nipkow [Mon, 28 Aug 2000 10:16:58 +0200] rev 9690
*** empty log message ***
doc-src/TutorialI/Recdef/Nested2.thy doc-src/TutorialI/Recdef/document/Nested2.tex

2000-08-28 nipkow [Mon, 28 Aug 2000 09:32:51 +0200] rev 9689
*** empty log message ***
doc-src/TutorialI/Datatype/ABexpr.thy doc-src/TutorialI/Datatype/Fundata.thy doc-src/TutorialI/Datatype/Nested.thy doc-src/TutorialI/Datatype/ROOT.ML doc-src/TutorialI/Datatype/document/ABexpr.tex doc-src/TutorialI/Datatype/document/Nested.tex doc-src/TutorialI/IsaMakefile doc-src/TutorialI/Misc/AdvancedInd.thy doc-src/TutorialI/Misc/Itrev.thy doc-src/TutorialI/Misc/def_rewr.thy doc-src/TutorialI/Recdef/Induction.thy doc-src/TutorialI/Recdef/Nested1.thy doc-src/TutorialI/Recdef/ROOT.ML doc-src/TutorialI/Recdef/document/Induction.tex doc-src/TutorialI/Trie/Trie.thy doc-src/TutorialI/basics.tex doc-src/TutorialI/fp.tex

2000-08-25 paulson [Fri, 25 Aug 2000 12:17:09 +0200] rev 9688
added \trivlist...\endtrivlist to the "isabelle" environment
in order to correct several problems (e.g. need for newlines and %)
lib/texinputs/isabelle.sty

2000-08-25 paulson [Fri, 25 Aug 2000 12:15:35 +0200] rev 9687
moved congruence rules UN_cong, INT_cong from UNTIY/Union to Set.ML
src/HOL/Set.ML src/HOL/UNITY/Union.ML

2000-08-24 paulson [Thu, 24 Aug 2000 12:39:42 +0200] rev 9686
xsymbols for {| and |}
src/HOL/Auth/Message.thy