| {date|age} |
@@ -36,3 +45,12 @@
{inbranch%inbranchtag}{branches%branchtag}{tags%tagtag}
+@@ -225,6 +226,7 @@
+ {desc|strip|firstline|escape|nonempty}
+
+
++ {author|person} |
+
+ file | diff | annotate {rename%filelogrename} |
+
'
+Only in isabelle/: map~
diff -r aace7a969410 -r 8629ac3efb19 Admin/isatest/isatest-stats
--- a/Admin/isatest/isatest-stats Tue May 04 19:57:55 2010 +0200
+++ b/Admin/isatest/isatest-stats Tue May 04 20:30:22 2010 +0200
@@ -6,7 +6,7 @@
THIS=$(cd "$(dirname "$0")"; pwd -P)
-PLATFORMS="at-poly at-poly-test at64-poly mac-poly-M4 mac-poly64-M4 mac-poly-M8 mac-poly64-M8 at-poly-5.1-para-e at64-poly-5.1-para at-mac-poly-5.1-para afp at-sml-dev sun-poly"
+PLATFORMS="at-poly at-poly-test at64-poly cygwin-poly mac-poly-M4 mac-poly64-M4 mac-poly-M8 mac-poly64-M8 at-poly-5.1-para-e at64-poly-5.1-para at-mac-poly-5.1-para afp at-sml-dev sun-poly"
ISABELLE_SESSIONS="\
HOL-Plain \
diff -r aace7a969410 -r 8629ac3efb19 CONTRIBUTORS
--- a/CONTRIBUTORS Tue May 04 19:57:55 2010 +0200
+++ b/CONTRIBUTORS Tue May 04 20:30:22 2010 +0200
@@ -6,6 +6,14 @@
Contributions to this Isabelle version
--------------------------------------
+* April 2010, Florian Haftmann, TUM
+ Reorganization of abstract algebra type classes.
+
+* April 2010, Florian Haftmann, TUM
+ Code generation for data representations involving invariants;
+ various collections avaiable in theories Fset, Dlist, RBT,
+ Mapping and AssocList.
+
Contributions to Isabelle2009-1
-------------------------------
diff -r aace7a969410 -r 8629ac3efb19 NEWS
--- a/NEWS Tue May 04 19:57:55 2010 +0200
+++ b/NEWS Tue May 04 20:30:22 2010 +0200
@@ -64,6 +64,11 @@
* Type constructors admit general mixfix syntax, not just infix.
+* Concrete syntax may be attached to local entities without a proof
+body, too. This works via regular mixfix annotations for 'fix',
+'def', 'obtain' etc. or via the explicit 'write' command, which is
+similar to the 'notation' command in theory specifications.
+
* Use of cumulative prems via "!" in some proof methods has been
discontinued (legacy feature).
@@ -84,6 +89,17 @@
*** Pure ***
+* Predicates of locales introduces by classes carry a mandatory "class"
+prefix. INCOMPATIBILITY.
+
+* 'code_reflect' allows to incorporate generated ML code into
+runtime environment; replaces immature code_datatype antiquotation.
+INCOMPATIBILITY.
+
+* Empty class specifications observe default sort. INCOMPATIBILITY.
+
+* Old 'axclass' has been discontinued. Use 'class' instead. INCOMPATIBILITY.
+
* Code generator: simple concept for abstract datatypes obeying invariants.
* Local theory specifications may depend on extra type variables that
@@ -103,6 +119,9 @@
datatype constructors have been renamed from InfixName to Infix etc.
Minor INCOMPATIBILITY.
+* Command 'example_proof' opens an empty proof body. This allows to
+experiment with Isar, without producing any persistent result.
+
* Commands 'type_notation' and 'no_type_notation' declare type syntax
within a local theory context, with explicit checking of the
constructors involved (in contrast to the raw 'syntax' versions).
@@ -111,6 +130,9 @@
context -- without introducing dependencies on parameters or
assumptions, which is not possible in Isabelle/Pure.
+* Command 'defaultsort' is renamed to 'default_sort', it works within
+a local theory context. Minor INCOMPATIBILITY.
+
* Proof terms: Type substitutions on proof constants now use canonical
order of type variables. INCOMPATIBILITY: Tools working with proof
terms may need to be adapted.
@@ -118,12 +140,8 @@
*** HOL ***
-* Abstract algebra:
- * class division_by_zero includes division_ring;
- * numerous lemmas have been ported from field to division_ring;
- * dropped lemma eq_minus_self_iff which is a duplicate for equal_neg_zero.
-
- INCOMPATIBILITY.
+* Theory 'Finite_Set': various folding_* locales facilitate the application
+of the various fold combinators on finite sets.
* Library theory 'RBT' renamed to 'RBT_Impl'; new library theory 'RBT'
provides abstract red-black tree type which is backed by RBT_Impl
@@ -153,16 +171,11 @@
INCOMPATIBILITY.
* Some generic constants have been put to appropriate theories:
-
- less_eq, less: Orderings
- zero, one, plus, minus, uminus, times, abs, sgn: Groups
- inverse, divide: Rings
-
+ * less_eq, less: Orderings
+ * zero, one, plus, minus, uminus, times, abs, sgn: Groups
+ * inverse, divide: Rings
INCOMPATIBILITY.
-* Class division_ring also requires proof of fact divide_inverse. However instantiation
-of parameter divide has also been required previously. INCOMPATIBILITY.
-
* More consistent naming of type classes involving orderings (and lattices):
lower_semilattice ~> semilattice_inf
@@ -214,33 +227,18 @@
INCOMPATIBILITY.
-* HOLogic.strip_psplit: types are returned in syntactic order, similar
-to other strip and tuple operations. INCOMPATIBILITY.
-
-* Various old-style primrec specifications in the HOL theories have been
-replaced by new-style primrec, especially in theory List. The corresponding
-constants now have authentic syntax. INCOMPATIBILITY.
-
-* Reorganized theory Multiset: swapped notation of pointwise and multiset order:
- * pointwise ordering is instance of class order with standard syntax <= and <;
- * multiset ordering has syntax <=# and <#; partial order properties are provided
- by means of interpretation with prefix multiset_order.
-Less duplication, less historical organization of sections,
-conversion from associations lists to multisets, rudimentary code generation.
-Use insert_DiffM2 [symmetric] instead of elem_imp_eq_diff_union, if needed.
-INCOMPATIBILITY.
-
-* Reorganized theory Sum_Type; Inl and Inr now have authentic syntax.
-INCOMPATIBILITY.
-
-* Code generation: ML and OCaml code is decorated with signatures.
-
-* Theory Complete_Lattice: lemmas top_def and bot_def have been
-replaced by the more convenient lemmas Inf_empty and Sup_empty.
-Dropped lemmas Inf_insert_simp and Sup_insert_simp, which are subsumed
-by Inf_insert and Sup_insert. Lemmas Inf_UNIV and Sup_UNIV replace
-former Inf_Univ and Sup_Univ. Lemmas inf_top_right and sup_bot_right
-subsume inf_top and sup_bot respectively. INCOMPATIBILITY.
+* Refined field classes:
+ * classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero
+ include rule inverse 0 = 0 -- subsumes former division_by_zero class.
+ * numerous lemmas have been ported from field to division_ring;
+ INCOMPATIBILITY.
+
+* Refined algebra theorem collections:
+ * dropped theorem group group_simps, use algebra_simps instead;
+ * dropped theorem group ring_simps, use field_simps instead;
+ * proper theorem collection field_simps subsumes former theorem groups field_eq_simps and field_simps;
+ * dropped lemma eq_minus_self_iff which is a duplicate for equal_neg_zero.
+ INCOMPATIBILITY.
* Theory Finite_Set and List: some lemmas have been generalized from
sets to lattices:
@@ -256,6 +254,27 @@
INTER_fold_inter ~> INFI_fold_inf
UNION_fold_union ~> SUPR_fold_sup
+* Theory Complete_Lattice: lemmas top_def and bot_def have been
+replaced by the more convenient lemmas Inf_empty and Sup_empty.
+Dropped lemmas Inf_insert_simp and Sup_insert_simp, which are subsumed
+by Inf_insert and Sup_insert. Lemmas Inf_UNIV and Sup_UNIV replace
+former Inf_Univ and Sup_Univ. Lemmas inf_top_right and sup_bot_right
+subsume inf_top and sup_bot respectively. INCOMPATIBILITY.
+
+* HOLogic.strip_psplit: types are returned in syntactic order, similar
+to other strip and tuple operations. INCOMPATIBILITY.
+
+* Reorganized theory Multiset: swapped notation of pointwise and multiset order:
+ * pointwise ordering is instance of class order with standard syntax <= and <;
+ * multiset ordering has syntax <=# and <#; partial order properties are provided
+ by means of interpretation with prefix multiset_order;
+ * less duplication, less historical organization of sections,
+ conversion from associations lists to multisets, rudimentary code generation;
+ * use insert_DiffM2 [symmetric] instead of elem_imp_eq_diff_union, if needed.
+ INCOMPATIBILITY.
+
+* Code generation: ML and OCaml code is decorated with signatures.
+
* Theory List: added transpose.
* Renamed Library/Quotient.thy to Library/Quotient_Type.thy to avoid
@@ -298,6 +317,14 @@
*** ML ***
+* Sorts.certify_sort and derived "cert" operations for types and terms
+no longer minimize sorts. Thus certification at the boundary of the
+inference kernel becomes invariant under addition of class relations,
+which is an important monotonicity principle. Sorts are now minimized
+in the syntax layer only, at the boundary between the end-user and the
+system. Subtle INCOMPATIBILITY, may have to use Sign.minimize_sort
+explicitly in rare situations.
+
* Antiquotations for basic formal entities:
@{class NAME} -- type class
@@ -341,6 +368,12 @@
* Configuration options now admit dynamic default values, depending on
the context or even global references.
+* Most operations that refer to a global context are named
+accordingly, e.g. Simplifier.global_context or
+ProofContext.init_global. There are some situations where a global
+context actually works, but under normal circumstances one needs to
+pass the proper local context through the code!
+
*** System ***
diff -r aace7a969410 -r 8629ac3efb19 doc-src/IsarImplementation/Thy/Logic.thy
--- a/doc-src/IsarImplementation/Thy/Logic.thy Tue May 04 19:57:55 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/Logic.thy Tue May 04 20:30:22 2010 +0200
@@ -128,8 +128,7 @@
@{index_ML Sign.subsort: "theory -> sort * sort -> bool"} \\
@{index_ML Sign.of_sort: "theory -> typ * sort -> bool"} \\
@{index_ML Sign.add_types: "(binding * int * mixfix) list -> theory -> theory"} \\
- @{index_ML Sign.add_tyabbrs_i: "
- (binding * string list * typ * mixfix) list -> theory -> theory"} \\
+ @{index_ML Sign.add_type_abbrev: "binding * string list * typ -> theory -> theory"} \\
@{index_ML Sign.primitive_class: "binding * class list -> theory -> theory"} \\
@{index_ML Sign.primitive_classrel: "class * class -> theory -> theory"} \\
@{index_ML Sign.primitive_arity: "arity -> theory -> theory"} \\
@@ -168,9 +167,9 @@
type constructors @{text "\