2007-09-26 wenzelm [Wed, 26 Sep 2007 20:50:34 +0200] rev 24732
added minimize_sort, complete_sort;
src/Pure/sign.ML src/Pure/sorts.ML

2007-09-26 wenzelm [Wed, 26 Sep 2007 20:50:33 +0200] rev 24731
Sign.minimize/complete_sort;
src/Pure/Isar/class.ML src/Pure/Isar/code.ML src/Pure/axclass.ML

2007-09-26 haftmann [Wed, 26 Sep 2007 20:27:58 +0200] rev 24730
convenient obtain rule for sets
src/HOL/Set.thy

2007-09-26 haftmann [Wed, 26 Sep 2007 20:27:57 +0200] rev 24729
added code lemma for 1
src/HOL/Nat.thy

2007-09-26 haftmann [Wed, 26 Sep 2007 20:27:55 +0200] rev 24728
moved Finite_Set before Datatype
src/HOL/Datatype.thy src/HOL/Equiv_Relations.thy src/HOL/Finite_Set.thy src/HOL/IntDef.thy src/HOLCF/Porder.thy

2007-09-26 wenzelm [Wed, 26 Sep 2007 19:19:38 +0200] rev 24727
adapted variable order for inductive cases (determined by read_specification *before* expanding abbreviations);
src/HOL/Bali/AxSound.thy src/HOL/Bali/Evaln.thy

2007-09-26 wenzelm [Wed, 26 Sep 2007 19:18:01 +0200] rev 24726
Attrib.eval_thms;
Syntax.parse/check;
src/ZF/Tools/inductive_package.ML

2007-09-26 wenzelm [Wed, 26 Sep 2007 19:18:00 +0200] rev 24725
Attrib.eval_thms;
src/ZF/Tools/datatype_package.ML src/ZF/Tools/induct_tacs.ML

2007-09-26 wenzelm [Wed, 26 Sep 2007 19:17:59 +0200] rev 24724
read/check_specification: proper type inference across multiple sections, result is in closed form;
added read/check_free_specification for single section, non-closed form;
src/Pure/Isar/specification.ML

2007-09-26 wenzelm [Wed, 26 Sep 2007 19:17:58 +0200] rev 24723
added eval_thms;
src/Pure/Isar/attrib.ML