2001-02-03 wenzelm [Sat, 03 Feb 2001 00:11:07 +0100] rev 11041
updated;
doc-src/IsarRef/intro.tex

2001-02-03 wenzelm [Sat, 03 Feb 2001 00:01:54 +0100] rev 11040
simplified 'split_format' syntax;
src/HOL/MicroJava/J/Eval.thy src/HOL/Tools/split_rule.ML

2001-02-02 wenzelm [Fri, 02 Feb 2001 23:59:30 +0100] rev 11039
'split_format' attribute;
doc-src/IsarRef/hol.tex

2001-02-02 wenzelm [Fri, 02 Feb 2001 22:21:06 +0100] rev 11038
tuned;
TFL/post.ML

2001-02-02 wenzelm [Fri, 02 Feb 2001 22:20:43 +0100] rev 11037
module setup;
use hidden internal_split constants;
src/HOL/Tools/split_rule.ML

2001-02-02 wenzelm [Fri, 02 Feb 2001 22:20:09 +0100] rev 11036
use hol_simplify;
src/HOL/Tools/inductive_package.ML

2001-02-02 wenzelm [Fri, 02 Feb 2001 22:19:52 +0100] rev 11035
use hol_rewrite_cterm;
src/HOL/Tools/induct_method.ML

2001-02-02 wenzelm [Fri, 02 Feb 2001 22:19:23 +0100] rev 11034
added hol_simplify, hol_rewrite_cterm;
src/HOL/simpdata.ML

2001-02-02 wenzelm [Fri, 02 Feb 2001 22:19:02 +0100] rev 11033
split = split_conv (for compatibility);
src/HOL/Product_Type_lemmas.ML

2001-02-02 wenzelm [Fri, 02 Feb 2001 22:18:10 +0100] rev 11032
added hidden internal_split constant;
tuned;
src/HOL/Product_Type.thy