wenzelm [Tue, 09 May 2000 15:10:25 +0200] rev 8845
updated keywords;
wenzelm [Tue, 09 May 2000 14:33:43 +0200] rev 8844
named "op ^" definitions;
wenzelm [Tue, 09 May 2000 14:16:32 +0200] rev 8843
improved X-Symbol stuff;
paulson [Tue, 09 May 2000 11:29:13 +0200] rev 8842
more examples
wenzelm [Mon, 08 May 2000 21:00:27 +0200] rev 8841
added INSTALL;
wenzelm [Mon, 08 May 2000 20:59:30 +0200] rev 8840
moved theory Sexp to Induct examples;
wenzelm [Mon, 08 May 2000 20:58:49 +0200] rev 8839
strip = impI allI allI;
wenzelm [Mon, 08 May 2000 20:57:02 +0200] rev 8838
replaced rabs by overloaded abs;
paulson [Mon, 08 May 2000 18:20:04 +0200] rev 8837
yet another example
paulson [Mon, 08 May 2000 16:59:18 +0200] rev 8836
new example
paulson [Mon, 08 May 2000 16:59:02 +0200] rev 8835
tidied
paulson [Mon, 08 May 2000 16:58:44 +0200] rev 8834
better simplification of the result of simprocs
paulson [Mon, 08 May 2000 16:58:18 +0200] rev 8833
moved le_square, proved le_cube
paulson [Mon, 08 May 2000 16:57:53 +0200] rev 8832
more details
wenzelm [Mon, 08 May 2000 11:45:57 +0200] rev 8831
tuned msg;
wenzelm [Mon, 08 May 2000 11:45:47 +0200] rev 8830
val needs_filtered_use = true;
wenzelm [Mon, 08 May 2000 11:35:19 +0200] rev 8829
recovered \seealso;
wenzelm [Mon, 08 May 2000 11:13:28 +0200] rev 8828
improved indexing;
wenzelm [Mon, 08 May 2000 11:13:11 +0200] rev 8827
\usepackage{makeidx};
wenzelm [Mon, 08 May 2000 11:03:53 +0200] rev 8826
tuned GARBAGE;
wenzelm [Mon, 08 May 2000 10:53:13 +0200] rev 8825
improved handling of Isabelle styles (less garbage);
wenzelm [Mon, 08 May 2000 10:52:46 +0200] rev 8824
updated;
wenzelm [Mon, 08 May 2000 10:52:28 +0200] rev 8823
updated syntax of simp options: (no_asm) etc.;
wenzelm [Mon, 08 May 2000 10:51:07 +0200] rev 8822
removed \isabelledefaultstyle (use \isabellestyle instead);
wenzelm [Mon, 08 May 2000 10:49:27 +0200] rev 8821
always discgarb -c;
wenzelm [Sat, 06 May 2000 00:46:13 +0200] rev 8820
fixed clash with new 'abs' const;
wenzelm [Fri, 05 May 2000 22:37:04 +0200] rev 8819
use Sign.simple_read_term;
wenzelm [Fri, 05 May 2000 22:35:51 +0200] rev 8818
error msg: counting from one (again), in order to be consistent with
case names of induction rule;