# HG changeset patch
# User wenzelm
# Date 1335629390 -7200
# Node ID 0e36cc70cb3ed3a1049c57abeaf571be18b6c7cd
# Parent  e6e1b670520b8c643360df109187e8075d5e4282
some re-ordering;

diff -r e6e1b670520b -r 0e36cc70cb3e NEWS
--- a/NEWS	Sat Apr 28 18:05:19 2012 +0200
+++ b/NEWS	Sat Apr 28 18:09:50 2012 +0200
@@ -20,29 +20,6 @@
 header -- minor INCOMPATIBILITY for user-defined commands.  Allow new
 commands to be used in the same theory where defined.
 
-* Rule attributes in local theory declarations (e.g. locale or class)
-are now statically evaluated: the resulting theorem is stored instead
-of the original expression.  INCOMPATIBILITY in rare situations, where
-the historic accident of dynamic re-evaluation in interpretations
-etc. was exploited.
-
-* Commands 'lemmas' and 'theorems' allow local variables using 'for'
-declaration, and results are standardized before being stored.  Thus
-old-style "standard" after instantiation or composition of facts
-becomes obsolete.  Minor INCOMPATIBILITY, due to potential change of
-indices of schematic variables.
-
-* Simplified configuration options for syntax ambiguity: see
-"syntax_ambiguity_warning" and "syntax_ambiguity_limit" in isar-ref
-manual.  Minor INCOMPATIBILITY.
-
-* Updated and extended reference manuals: "isar-ref",
-"implementation", "system"; reduced remaining material in old "ref"
-manual.
-
-
-*** Pure ***
-
 * Auxiliary contexts indicate block structure for specifications with
 additional parameters and assumptions.  Such unnamed contexts may be
 nested within other targets, like 'theory', 'locale', 'class',
@@ -75,6 +52,36 @@
 See commands 'bundle', 'include', 'including' etc. in the isar-ref
 manual.
 
+* Commands 'lemmas' and 'theorems' allow local variables using 'for'
+declaration, and results are standardized before being stored.  Thus
+old-style "standard" after instantiation or composition of facts
+becomes obsolete.  Minor INCOMPATIBILITY, due to potential change of
+indices of schematic variables.
+
+* Rule attributes in local theory declarations (e.g. locale or class)
+are now statically evaluated: the resulting theorem is stored instead
+of the original expression.  INCOMPATIBILITY in rare situations, where
+the historic accident of dynamic re-evaluation in interpretations
+etc. was exploited.
+
+* New tutorial "Programming and Proving in Isabelle/HOL"
+("prog-prove").  It completely supersedes "A Tutorial Introduction to
+Structured Isar Proofs" ("isar-overview"), which has been removed.  It
+also supersedes "Isabelle/HOL, A Proof Assistant for Higher-Order
+Logic" as the recommended beginners tutorial, but does not cover all
+of the material of that old tutorial.
+
+* Updated and extended reference manuals: "isar-ref",
+"implementation", "system"; reduced remaining material in old "ref"
+manual.
+
+
+*** Pure ***
+
+* Discontinued old "prems" fact, which used to refer to the accidental
+collection of foundational premises in the context (already marked as
+legacy since Isabelle2011).
+
 * Rule composition via attribute "OF" (or ML functions OF/MRS) is more
 tolerant against multiple unifiers, as long as the final result is
 unique.  (As before, rules are composed in canonical right-to-left
@@ -94,15 +101,15 @@
 "num_position" etc. are mainly used instead (which also include
 position information via constraints).
 
+* Simplified configuration options for syntax ambiguity: see
+"syntax_ambiguity_warning" and "syntax_ambiguity_limit" in isar-ref
+manual.  Minor INCOMPATIBILITY.
+
 * Attribute "abs_def" turns an equation of the form "f x y == t" into
 "f == %x y. t", which ensures that "simp" or "unfold" steps always
 expand it.  This also works for object-logic equality.  (Formerly
 undocumented feature.)
 
-* Discontinued old "prems" fact, which used to refer to the accidental
-collection of foundational premises in the context (already marked as
-legacy since Isabelle2011).
-
 * Obsolete command 'types' has been discontinued.  Use 'type_synonym'
 instead.  INCOMPATIBILITY.
 
@@ -132,13 +139,6 @@
 
 *** HOL ***
 
-* New tutorial "Programming and Proving in Isabelle/HOL"
-("prog-prove").  It completely supersedes "A Tutorial Introduction to
-Structured Isar Proofs" ("isar-overview"), which has been removed.  It
-also supersedes "Isabelle/HOL, A Proof Assistant for Higher-Order
-Logic" as the recommended beginners tutorial, but does not cover all
-of the material of that old tutorial.
-
 * Type 'a set is now a proper type constructor (just as before
 Isabelle2008).  Definitions mem_def and Collect_def have disappeared.
 Non-trivial INCOMPATIBILITY.  For developments keeping predicates and
@@ -180,10 +180,10 @@
 * Code generation by default implements sets as container type rather
 than predicates.  INCOMPATIBILITY.
 
-* New proof import from HOL Light: Faster, simpler, and more scalable.
-Requires a proof bundle, which is available as an external component.
-Discontinued old (and mostly dead) Importer for HOL4 and HOL Light.
-INCOMPATIBILITY.
+* HOL-Import: Re-implementation from scratch is faster, simpler, and
+more scalable.  Requires a proof bundle, which is available as an
+external component.  Discontinued old (and mostly dead) Importer for
+HOL4 and HOL Light.  INCOMPATIBILITY.
 
 * New type synonym 'a rel = ('a * 'a) set