NEWS
changeset 47829 0e36cc70cb3e
parent 47827 13530d774a21
child 47842 bfc08ce7b7b9
     1.1 --- a/NEWS	Sat Apr 28 18:05:19 2012 +0200
     1.2 +++ b/NEWS	Sat Apr 28 18:09:50 2012 +0200
     1.3 @@ -20,29 +20,6 @@
     1.4  header -- minor INCOMPATIBILITY for user-defined commands.  Allow new
     1.5  commands to be used in the same theory where defined.
     1.6  
     1.7 -* Rule attributes in local theory declarations (e.g. locale or class)
     1.8 -are now statically evaluated: the resulting theorem is stored instead
     1.9 -of the original expression.  INCOMPATIBILITY in rare situations, where
    1.10 -the historic accident of dynamic re-evaluation in interpretations
    1.11 -etc. was exploited.
    1.12 -
    1.13 -* Commands 'lemmas' and 'theorems' allow local variables using 'for'
    1.14 -declaration, and results are standardized before being stored.  Thus
    1.15 -old-style "standard" after instantiation or composition of facts
    1.16 -becomes obsolete.  Minor INCOMPATIBILITY, due to potential change of
    1.17 -indices of schematic variables.
    1.18 -
    1.19 -* Simplified configuration options for syntax ambiguity: see
    1.20 -"syntax_ambiguity_warning" and "syntax_ambiguity_limit" in isar-ref
    1.21 -manual.  Minor INCOMPATIBILITY.
    1.22 -
    1.23 -* Updated and extended reference manuals: "isar-ref",
    1.24 -"implementation", "system"; reduced remaining material in old "ref"
    1.25 -manual.
    1.26 -
    1.27 -
    1.28 -*** Pure ***
    1.29 -
    1.30  * Auxiliary contexts indicate block structure for specifications with
    1.31  additional parameters and assumptions.  Such unnamed contexts may be
    1.32  nested within other targets, like 'theory', 'locale', 'class',
    1.33 @@ -75,6 +52,36 @@
    1.34  See commands 'bundle', 'include', 'including' etc. in the isar-ref
    1.35  manual.
    1.36  
    1.37 +* Commands 'lemmas' and 'theorems' allow local variables using 'for'
    1.38 +declaration, and results are standardized before being stored.  Thus
    1.39 +old-style "standard" after instantiation or composition of facts
    1.40 +becomes obsolete.  Minor INCOMPATIBILITY, due to potential change of
    1.41 +indices of schematic variables.
    1.42 +
    1.43 +* Rule attributes in local theory declarations (e.g. locale or class)
    1.44 +are now statically evaluated: the resulting theorem is stored instead
    1.45 +of the original expression.  INCOMPATIBILITY in rare situations, where
    1.46 +the historic accident of dynamic re-evaluation in interpretations
    1.47 +etc. was exploited.
    1.48 +
    1.49 +* New tutorial "Programming and Proving in Isabelle/HOL"
    1.50 +("prog-prove").  It completely supersedes "A Tutorial Introduction to
    1.51 +Structured Isar Proofs" ("isar-overview"), which has been removed.  It
    1.52 +also supersedes "Isabelle/HOL, A Proof Assistant for Higher-Order
    1.53 +Logic" as the recommended beginners tutorial, but does not cover all
    1.54 +of the material of that old tutorial.
    1.55 +
    1.56 +* Updated and extended reference manuals: "isar-ref",
    1.57 +"implementation", "system"; reduced remaining material in old "ref"
    1.58 +manual.
    1.59 +
    1.60 +
    1.61 +*** Pure ***
    1.62 +
    1.63 +* Discontinued old "prems" fact, which used to refer to the accidental
    1.64 +collection of foundational premises in the context (already marked as
    1.65 +legacy since Isabelle2011).
    1.66 +
    1.67  * Rule composition via attribute "OF" (or ML functions OF/MRS) is more
    1.68  tolerant against multiple unifiers, as long as the final result is
    1.69  unique.  (As before, rules are composed in canonical right-to-left
    1.70 @@ -94,15 +101,15 @@
    1.71  "num_position" etc. are mainly used instead (which also include
    1.72  position information via constraints).
    1.73  
    1.74 +* Simplified configuration options for syntax ambiguity: see
    1.75 +"syntax_ambiguity_warning" and "syntax_ambiguity_limit" in isar-ref
    1.76 +manual.  Minor INCOMPATIBILITY.
    1.77 +
    1.78  * Attribute "abs_def" turns an equation of the form "f x y == t" into
    1.79  "f == %x y. t", which ensures that "simp" or "unfold" steps always
    1.80  expand it.  This also works for object-logic equality.  (Formerly
    1.81  undocumented feature.)
    1.82  
    1.83 -* Discontinued old "prems" fact, which used to refer to the accidental
    1.84 -collection of foundational premises in the context (already marked as
    1.85 -legacy since Isabelle2011).
    1.86 -
    1.87  * Obsolete command 'types' has been discontinued.  Use 'type_synonym'
    1.88  instead.  INCOMPATIBILITY.
    1.89  
    1.90 @@ -132,13 +139,6 @@
    1.91  
    1.92  *** HOL ***
    1.93  
    1.94 -* New tutorial "Programming and Proving in Isabelle/HOL"
    1.95 -("prog-prove").  It completely supersedes "A Tutorial Introduction to
    1.96 -Structured Isar Proofs" ("isar-overview"), which has been removed.  It
    1.97 -also supersedes "Isabelle/HOL, A Proof Assistant for Higher-Order
    1.98 -Logic" as the recommended beginners tutorial, but does not cover all
    1.99 -of the material of that old tutorial.
   1.100 -
   1.101  * Type 'a set is now a proper type constructor (just as before
   1.102  Isabelle2008).  Definitions mem_def and Collect_def have disappeared.
   1.103  Non-trivial INCOMPATIBILITY.  For developments keeping predicates and
   1.104 @@ -180,10 +180,10 @@
   1.105  * Code generation by default implements sets as container type rather
   1.106  than predicates.  INCOMPATIBILITY.
   1.107  
   1.108 -* New proof import from HOL Light: Faster, simpler, and more scalable.
   1.109 -Requires a proof bundle, which is available as an external component.
   1.110 -Discontinued old (and mostly dead) Importer for HOL4 and HOL Light.
   1.111 -INCOMPATIBILITY.
   1.112 +* HOL-Import: Re-implementation from scratch is faster, simpler, and
   1.113 +more scalable.  Requires a proof bundle, which is available as an
   1.114 +external component.  Discontinued old (and mostly dead) Importer for
   1.115 +HOL4 and HOL Light.  INCOMPATIBILITY.
   1.116  
   1.117  * New type synonym 'a rel = ('a * 'a) set
   1.118