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
wenzelm [Thu, 24 Aug 2000 00:55:42 +0200] rev 9682
more symbols;
wenzelm [Thu, 24 Aug 2000 00:54:54 +0200] rev 9681
disabled trivlist (causes non-descript problems in HOL-Real-HahnBanach);
wenzelm [Thu, 24 Aug 2000 00:53:53 +0200] rev 9680
choosefrom: support easy settings;
wenzelm [Thu, 24 Aug 2000 00:53:23 +0200] rev 9679
choosefrom: easy settings;
wenzelm [Wed, 23 Aug 2000 15:24:46 +0200] rev 9678
isabelle env: trivlist;
paulson [Tue, 22 Aug 2000 11:24:44 +0200] rev 9677
removed redundant commands