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
paulson [Tue, 22 Aug 2000 11:24:24 +0200] rev 9676
removed most "makeatother", no longer needed
paulson [Tue, 22 Aug 2000 10:59:15 +0200] rev 9675
updated to latest versions of ttbox and ttbreak
wenzelm [Mon, 21 Aug 2000 19:29:27 +0200] rev 9674
updated;
wenzelm [Mon, 21 Aug 2000 19:17:07 +0200] rev 9673
updated;
wenzelm [Mon, 21 Aug 2000 19:03:58 +0200] rev 9672
updated;
wenzelm [Mon, 21 Aug 2000 18:49:38 +0200] rev 9671
tuned translations;
nipkow [Mon, 21 Aug 2000 18:45:29 +0200] rev 9670
*** empty log message ***
wenzelm [Mon, 21 Aug 2000 18:40:30 +0200] rev 9669
added \isastyleminor;
more \isachars;
added \isadigit;
improved \isakeyword;
tuned;
wenzelm [Mon, 21 Aug 2000 18:38:27 +0200] rev 9668
more \isachars;
added \isadigit;
simplified command markup;
wenzelm [Mon, 21 Aug 2000 18:16:47 +0200] rev 9667
fixed has_meta_prems: strip_assums_hyp;
nipkow [Mon, 21 Aug 2000 17:54:43 +0200] rev 9666
*** empty log message ***
wenzelm [Mon, 21 Aug 2000 13:47:24 +0200] rev 9665
updated;
wenzelm [Sun, 20 Aug 2000 17:45:20 +0200] rev 9664
open cases;
wenzelm [Sat, 19 Aug 2000 12:49:19 +0200] rev 9663
output \isachar;
wenzelm [Sat, 19 Aug 2000 12:48:26 +0200] rev 9662
cond_add_path;
wenzelm [Sat, 19 Aug 2000 12:47:16 +0200] rev 9661
fixed text;
wenzelm [Sat, 19 Aug 2000 12:45:11 +0200] rev 9660
turned into new-style theory;
wenzelm [Sat, 19 Aug 2000 12:44:39 +0200] rev 9659
tuned;
wenzelm [Sat, 19 Aug 2000 12:44:20 +0200] rev 9658
tuned \isastyle;
wenzelm [Sat, 19 Aug 2000 12:43:55 +0200] rev 9657
added \isachar definitions;
added \isabellestyle switch;
tuned;
wenzelm [Sat, 19 Aug 2000 12:42:52 +0200] rev 9656
%\urlstyle{rm}
%\isabellestyle{it}
wenzelm [Sat, 19 Aug 2000 12:41:41 +0200] rev 9655
renamed cond_with_path to cond_add_path (add to front);
improved with_path(s) (add to rear);
paulson [Fri, 18 Aug 2000 18:46:02 +0200] rev 9654
X-symbols for ordinal, cardinal, integer arithmetic