--- a/NEWS Tue Oct 23 23:27:23 2007 +0200
+++ b/NEWS Wed Oct 24 07:19:52 2007 +0200
@@ -823,7 +823,7 @@
package; constants add, mul, pow now curried. Infix syntax for
algebraic operations.
-* Some steps towards more uniform lattice theory development in HOL.
+* More uniform lattice theory development in HOL.
constants "meet" and "join" now named "inf" and "sup"
constant "Meet" now named "Inf"
@@ -946,6 +946,9 @@
* Classes "order" and "linorder": potential INCOMPATIBILITY due to
changed order of proof goals instance proofs.
+* Locale "partial_order" now unified with class "order" (cf. theory
+Orderings), added parameter "less". INCOMPATIBILITY.
+
* Dropped redundant lemma def_imp_eq in favor of meta_eq_to_obj_eq.
INCOMPATIBILITY.
@@ -977,10 +980,7 @@
* Class "recpower" is generalized to arbitrary monoids, not just
commutative semirings. INCOMPATIBILITY: may need to incorporate
-commutativity or a semiring properties additionally.
-
-* Unified locale "partial_order" with class definition (cf. theory
-Orderings), added parameter "less". INCOMPATIBILITY.
+commutativity or semiring properties additionally.
* Constant "List.list_all2" in List.thy now uses authentic syntax.
INCOMPATIBILITY: translations containing list_all2 may go wrong,
@@ -1005,11 +1005,12 @@
See HOL/Integ/IntArith.thy for an example setup.
-* New top level command 'normal_form' computes the normal form of a
-term that may contain free variables. For example ``normal_form
-"rev[a,b,c]"'' produces ``[b,c,a]'' (without proof). This command is
-suitable for heavy-duty computations because the functions are
-compiled to ML first.
+* Command 'normal_form' computes the normal form of a
+term that may contain free variables. For example
+``normal_form "rev [a, b, c]"'' produces ``[b, c, a]'' (without proof).
+This command is suitable for heavy-duty computations because the functions
+are compiled to ML first. Correspondingly, a method ``normalization''
+is provided. See further HOL/ex/NormalForm.thy and Tools/nbe.ML.
* Alternative iff syntax "A <-> B" for equality on bool (with priority
25 like -->); output depends on the "iff" print_mode, the default is
--- a/src/Pure/Isar/class.ML Tue Oct 23 23:27:23 2007 +0200
+++ b/src/Pure/Isar/class.ML Wed Oct 24 07:19:52 2007 +0200
@@ -433,16 +433,13 @@
(* updaters *)
-fun add_class_data ((class, superclasses), (cs, base_sort, insttab, phi, intro)) thy =
+fun add_class_data ((class, superclasses), (cs, base_sort, inst, phi, intro)) thy =
let
- val inst = map
- (SOME o the o Symtab.lookup insttab o fst o fst)
- (Locale.parameters_of_expr thy (Locale.Locale class));
val operations = map (fn (v_ty as (_, ty'), (c, ty)) =>
(c, ((Free v_ty, (Logic.varifyT ty, 0)), (Free v_ty, ty')))) cs;
val cs = (map o pairself) fst cs;
val add_class = Graph.new_node (class,
- mk_class_data ((cs, base_sort, inst, phi, intro), ([], operations)))
+ mk_class_data ((cs, base_sort, map (SOME o Const) inst, phi, intro), ([], operations)))
#> fold (curry Graph.add_edge class) superclasses;
in
ClassData.map add_class thy
@@ -738,10 +735,8 @@
val (((sups, supconsts), (supsort, base_sort, mergeexpr)), elems_syn) =
prep_spec thy raw_supclasses raw_includes_elems;
val other_consts = map (tap (Sign.the_const_type thy) o prep_param thy) raw_other_consts;
- fun mk_inst class param_names cs =
- Symtab.empty
- |> fold2 (fn v => fn (c, ty) => Symtab.update (v, Const
- (c, Term.map_type_tfree (fn (v, _) => TFree (v, [class])) ty))) param_names cs;
+ fun mk_inst class cs =
+ (map o apsnd o Term.map_type_tfree) (fn (v, _) => TFree (v, [class])) cs;
fun fork_syntax (Element.Fixes xs) =
fold_map (fn (c, ty, syn) => cons (c, syn) #> pair (c, ty, NoSyn)) xs
#>> Element.Fixes
@@ -785,7 +780,7 @@
#-> (fn [(_, [class_intro])] =>
add_class_data ((class, sups),
(map fst params ~~ consts, base_sort,
- mk_inst class (map fst all_params) (map snd supconsts @ consts),
+ mk_inst class (map snd supconsts @ consts),
calculate_morphism class (supconsts @ (map (fst o fst) params ~~ consts)), class_intro))
#> class_interpretation class axioms []
)))))