2007-12-03 haftmann [Mon, 03 Dec 2007 16:04:16 +0100] rev 25518
interface for unchecked definitions
src/Pure/Isar/class.ML src/Pure/more_thm.ML

2007-12-03 haftmann [Mon, 03 Dec 2007 16:04:14 +0100] rev 25517
shifted "fun" command to Wellfounded_Relations
src/HOL/PreList.thy src/HOL/Wellfounded_Relations.thy

2007-12-03 haftmann [Mon, 03 Dec 2007 16:04:13 +0100] rev 25516
updated
etc/isar-keywords-ZF.el etc/isar-keywords.el lib/jedit/isabelle.xml

2007-12-02 chaieb [Sun, 02 Dec 2007 20:38:42 +0100] rev 25515
Eliminated unused theorems minusinf_ex and minusinf_bex
src/HOL/ex/Reflected_Presburger.thy

2007-11-30 haftmann [Fri, 30 Nov 2007 20:13:08 +0100] rev 25514
first working version of instance target
src/Pure/Isar/class.ML src/Pure/Isar/instance.ML src/Pure/Isar/theory_target.ML

2007-11-30 haftmann [Fri, 30 Nov 2007 20:13:07 +0100] rev 25513
interpretation for typedefs
src/HOL/Tools/typedef_package.ML

2007-11-30 haftmann [Fri, 30 Nov 2007 20:13:06 +0100] rev 25512
using intro_locales instead of unfold_locales if appropriate
src/HOL/OrderedGroup.thy src/HOL/Ring_and_Field.thy

2007-11-30 haftmann [Fri, 30 Nov 2007 20:13:05 +0100] rev 25511
more canonical attribute application
src/HOL/Bali/State.thy src/HOL/Datatype.thy src/HOL/Product_Type.thy

2007-11-30 haftmann [Fri, 30 Nov 2007 20:13:03 +0100] rev 25510
adjustions to due to instance target
NEWS src/HOL/Inductive.thy src/HOL/Lattices.thy src/HOL/Nat.thy src/HOL/Orderings.thy src/HOL/Set.thy src/HOL/Tools/inductive_package.ML

2007-11-30 krauss [Fri, 30 Nov 2007 16:23:52 +0100] rev 25509
new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
src/HOL/Tools/function_package/lexicographic_order.ML