wenzelm [Mon, 28 Aug 2000 13:48:25 +0200] rev 9692
proper setup;
wenzelm [Mon, 28 Aug 2000 13:48:14 +0200] rev 9691
removed ttbox;
nipkow [Mon, 28 Aug 2000 10:16:58 +0200] rev 9690
*** empty log message ***
nipkow [Mon, 28 Aug 2000 09:32:51 +0200] rev 9689
*** empty log message ***
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 %)
paulson [Fri, 25 Aug 2000 12:15:35 +0200] rev 9687
moved congruence rules UN_cong, INT_cong from UNTIY/Union to Set.ML
paulson [Thu, 24 Aug 2000 12:39:42 +0200] rev 9686
xsymbols for {| and |}
paulson [Thu, 24 Aug 2000 12:39:24 +0200] rev 9685
xsymbols for leads-to and Join
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;
paulson [Thu, 24 Aug 2000 11:05:20 +0200] rev 9683
added some xsymbols, and tidied