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

2001-02-02 wenzelm [Fri, 02 Feb 2001 22:17:31 +0100] rev 11031
isatool convert;
doc-src/System/misc.tex

2001-02-02 paulson [Fri, 02 Feb 2001 11:42:36 +0100] rev 11030
new theorem fib_mult_eq_setsum
src/HOL/NumberTheory/Fib.ML

2001-02-02 oheimb [Fri, 02 Feb 2001 00:31:39 +0100] rev 11029
little bugfixes; added induct_thm_tac
lib/scripts/convert.pl

2001-02-01 wenzelm [Thu, 01 Feb 2001 21:28:23 +0100] rev 11028
moved to Product_Type_lemmas.ML
src/HOL/Product_Type.ML

2001-02-01 oheimb [Thu, 01 Feb 2001 20:56:21 +0100] rev 11027
added translations for bind_thm and val
lib/scripts/convert.pl

2001-02-01 oheimb [Thu, 01 Feb 2001 20:53:13 +0100] rev 11026
converted to Isar, simplifying recursion on class hierarchy
src/HOL/IsaMakefile src/HOL/MicroJava/BV/BVSpec.thy src/HOL/MicroJava/J/Conform.ML src/HOL/MicroJava/J/Conform.thy src/HOL/MicroJava/J/Decl.ML src/HOL/MicroJava/J/Decl.thy src/HOL/MicroJava/J/Eval.ML src/HOL/MicroJava/J/Eval.thy src/HOL/MicroJava/J/Example.ML src/HOL/MicroJava/J/Example.thy src/HOL/MicroJava/J/JBasis.ML src/HOL/MicroJava/J/JBasis.thy src/HOL/MicroJava/J/JTypeSafe.ML src/HOL/MicroJava/J/JTypeSafe.thy src/HOL/MicroJava/J/State.ML src/HOL/MicroJava/J/State.thy src/HOL/MicroJava/J/Term.thy src/HOL/MicroJava/J/Type.thy src/HOL/MicroJava/J/TypeRel.ML src/HOL/MicroJava/J/TypeRel.thy src/HOL/MicroJava/J/Value.thy src/HOL/MicroJava/J/WellForm.ML src/HOL/MicroJava/J/WellForm.thy src/HOL/MicroJava/J/WellType.ML src/HOL/MicroJava/J/WellType.thy src/HOL/MicroJava/ROOT.ML