# HG changeset patch
# User haftmann
# Date 1162904584 -3600
# Node ID 7c9337a0e30a4a616f7849f4f407b6889708471e
# Parent  a91bab12b2bd0531d371022b7fed81c3e11c96f4
made locale partial_order compatible with axclass order

diff -r a91bab12b2bd -r 7c9337a0e30a NEWS
--- 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
diff -r a91bab12b2bd -r 7c9337a0e30a src/HOL/Finite_Set.thy
--- 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)