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

2000-08-24 paulson [Thu, 24 Aug 2000 12:39:24 +0200] rev 9685
xsymbols for leads-to and Join
src/HOL/UNITY/SubstAx.thy src/HOL/UNITY/Union.thy src/HOL/UNITY/WFair.thy

2000-08-24 paulson [Thu, 24 Aug 2000 11:14:21 +0200] rev 9684
fixed strip_assums and assum_pairs, restoring them (essentially) to their
1989 versions. They had been "optimized" for flattened parameters, but
failed when given an initial, non-flattened proof state. A manifestation
of the bug is

Goal "of the bug isf. EX B. Q(f,B) ==> (of the bug isy. P(f,y))";
be exE 1;
src/Pure/logic.ML

2000-08-24 paulson [Thu, 24 Aug 2000 11:05:20 +0200] rev 9683
added some xsymbols, and tidied
src/ZF/AC/AC18_AC19.ML src/ZF/AC/AC7_AC9.ML src/ZF/AC/AC_Equiv.ML src/ZF/AC/DC.ML src/ZF/Arith.thy src/ZF/Cardinal.ML src/ZF/Cardinal.thy src/ZF/CardinalArith.thy src/ZF/Coind/Map.ML src/ZF/Order.thy src/ZF/OrderType.thy src/ZF/ZF.thy src/ZF/func.ML