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

2000-08-24 wenzelm [Thu, 24 Aug 2000 00:55:42 +0200] rev 9682
more symbols;
lib/texinputs/isabellesym.sty

2000-08-24 wenzelm [Thu, 24 Aug 2000 00:54:54 +0200] rev 9681
disabled trivlist (causes non-descript problems in HOL-Real-HahnBanach);
lib/texinputs/isabelle.sty

2000-08-24 wenzelm [Thu, 24 Aug 2000 00:53:53 +0200] rev 9680
choosefrom: support easy settings;
lib/scripts/getsettings

2000-08-24 wenzelm [Thu, 24 Aug 2000 00:53:23 +0200] rev 9679
choosefrom: easy settings;
etc/settings

2000-08-23 wenzelm [Wed, 23 Aug 2000 15:24:46 +0200] rev 9678
isabelle env: trivlist;
lib/texinputs/isabelle.sty

2000-08-22 paulson [Tue, 22 Aug 2000 11:24:44 +0200] rev 9677
removed redundant commands
doc-src/Tutorial/tutorial.tex doc-src/TutorialI/tutorial.tex

2000-08-22 paulson [Tue, 22 Aug 2000 11:24:24 +0200] rev 9676
removed most "makeatother", no longer needed
doc-src/Tutorial/fp.tex