--- a/NEWS Tue Nov 07 14:02:10 2006 +0100
+++ b/NEWS Tue Nov 07 14:03:04 2006 +0100
@@ -87,7 +87,8 @@
For code_instance and code_class, target SML is silently ignored.
-See HOL theories and HOL/ex/Code*.thy for usage examples.
+See HOL theories and HOL/ex/Code*.thy for usage examples. Doc/Isar/Advanced/Codegen/
+provides a tutorial.
* Command 'no_translations' removes translation rules from theory
syntax.
@@ -487,6 +488,12 @@
INCOMPATIBILITY: If you use recpower and need commutativity or a semiring
property, add the corresponding classes.
+* Locale Lattic_Locales.partial_order changed (to achieve consistency with
+ axclass order):
+ - moved to Orderings.partial_order
+ - additional parameter ``less''
+ INCOMPATIBILITY.
+
* Constant "List.list_all2" in List.thy now uses authentic syntax.
INCOMPATIBILITY: translations containing list_all2 may go wrong. On Isar
level, use abbreviations instead.
@@ -501,7 +508,7 @@
INCOMPATIBILITY: ML code directly refering to constant names may need adaption
This in general only affects hand-written proof tactics, simprocs and so on.
-* New theory OperationalEquality providing class 'eq' with constant 'eq',
+* New theory Code_Generator providing class 'eq' with constant 'eq',
allowing for code generation with polymorphic equality.
* Numeral syntax: type 'bin' which was a mere type copy of 'int' has been
--- a/src/HOL/Finite_Set.thy Tue Nov 07 14:02:10 2006 +0100
+++ b/src/HOL/Finite_Set.thy Tue Nov 07 14:03:04 2006 +0100
@@ -2411,7 +2411,7 @@
done
interpretation min_max:
- Lattice ["op \<le>" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "max" "Min" "Max"]
+ Lattice ["op \<le>" "op <" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "max" "Min" "Max"]
apply -
apply(rule Min_def)
apply(rule Max_def)
@@ -2420,7 +2420,7 @@
interpretation min_max:
- Distrib_Lattice ["op \<le>" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "max" "Min" "Max"]
+ Distrib_Lattice ["op \<le>" "op <" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "max" "Min" "Max"]
by unfold_locales
@@ -2588,7 +2588,7 @@
lemma inj_graph: "inj (%f. {(x, y). y = f x})"
by (rule inj_onI, auto simp add: expand_set_eq expand_fun_eq)
-instance fun :: (finite, finite) finite
+instance "fun" :: (finite, finite) finite
proof
show "finite (UNIV :: ('a => 'b) set)"
proof (rule finite_imageD)