Mon, 28 Aug 2000 10:16:58 +0200 *** empty log message ***
nipkow [Mon, 28 Aug 2000 10:16:58 +0200] rev 9690
*** empty log message ***
Mon, 28 Aug 2000 09:32:51 +0200 *** empty log message ***
nipkow [Mon, 28 Aug 2000 09:32:51 +0200] rev 9689
*** empty log message ***
Fri, 25 Aug 2000 12:17:09 +0200 added \trivlist...\endtrivlist to the "isabelle" environment
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 %)
Fri, 25 Aug 2000 12:15:35 +0200 moved congruence rules UN_cong, INT_cong from UNTIY/Union to Set.ML
paulson [Fri, 25 Aug 2000 12:15:35 +0200] rev 9687
moved congruence rules UN_cong, INT_cong from UNTIY/Union to Set.ML
Thu, 24 Aug 2000 12:39:42 +0200 xsymbols for {| and |}
paulson [Thu, 24 Aug 2000 12:39:42 +0200] rev 9686
xsymbols for {| and |}
Thu, 24 Aug 2000 12:39:24 +0200 xsymbols for leads-to and Join
paulson [Thu, 24 Aug 2000 12:39:24 +0200] rev 9685
xsymbols for leads-to and Join
Thu, 24 Aug 2000 11:14:21 +0200 fixed strip_assums and assum_pairs, restoring them (essentially) to their
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;
Thu, 24 Aug 2000 11:05:20 +0200 added some xsymbols, and tidied
paulson [Thu, 24 Aug 2000 11:05:20 +0200] rev 9683
added some xsymbols, and tidied
Thu, 24 Aug 2000 00:55:42 +0200 more symbols;
wenzelm [Thu, 24 Aug 2000 00:55:42 +0200] rev 9682
more symbols;
Thu, 24 Aug 2000 00:54:54 +0200 disabled trivlist (causes non-descript problems in HOL-Real-HahnBanach);
wenzelm [Thu, 24 Aug 2000 00:54:54 +0200] rev 9681
disabled trivlist (causes non-descript problems in HOL-Real-HahnBanach);
(0) -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip