src/HOL/Algebra/IntRing.thy

--- a/src/HOL/Algebra/IntRing.thy	Fri Jan 12 09:58:31 2007 +0100
+++ b/src/HOL/Algebra/IntRing.thy	Fri Jan 12 15:37:21 2007 +0100
@@ -96,54 +96,60 @@
 interpretation "domain" ["\<Z>"] by (rule int_is_domain)
 
 lemma int_le_total_order:
-  "total_order (UNIV::int set) (op \<le>)"
-apply (rule partial_order.total_orderI)
- apply (rule partial_order.intro, simp+)
-apply clarsimp
-done
+  "total_order (| carrier = UNIV::int set, le = op \<le> |)"
+  apply (rule partial_order.total_orderI)
+   apply (rule partial_order.intro, simp+)
+  apply clarsimp
+  done
 
 lemma less_int:
-  "order_syntax.less (op \<le>::[int, int] => bool) = (op <)"
-  by (auto simp add: expand_fun_eq order_syntax.less_def)
+  "lless (| carrier = UNIV::int set, le = op \<le> |) = (op <)"
+  by (auto simp add: expand_fun_eq lless_def)
 
 lemma join_int:
-  "order_syntax.join (UNIV::int set) (op \<le>) = max"
+  "join (| carrier = UNIV::int set, le = op \<le> |) = max"
   apply (simp add: expand_fun_eq max_def)
   apply (rule+)
   apply (rule lattice.joinI)
   apply (simp add: int_le_total_order total_order.axioms)
-  apply (simp add: order_syntax.least_def order_syntax.Upper_def)
+  apply (simp add: least_def Upper_def)
   apply arith
   apply simp apply simp
   apply (rule lattice.joinI)
   apply (simp add: int_le_total_order total_order.axioms)
-  apply (simp add: order_syntax.least_def order_syntax.Upper_def)
+  apply (simp add: least_def Upper_def)
   apply arith
   apply simp apply simp
   done
 
 lemma meet_int:
-  "order_syntax.meet (UNIV::int set) (op \<le>) = min"
+  "meet (| carrier = UNIV::int set, le = op \<le> |) = min"
   apply (simp add: expand_fun_eq min_def)
   apply (rule+)
   apply (rule lattice.meetI)
   apply (simp add: int_le_total_order total_order.axioms)
-  apply (simp add: order_syntax.greatest_def order_syntax.Lower_def)
+  apply (simp add: greatest_def Lower_def)
   apply arith
   apply simp apply simp
   apply (rule lattice.meetI)
   apply (simp add: int_le_total_order total_order.axioms)
-  apply (simp add: order_syntax.greatest_def order_syntax.Lower_def)
+  apply (simp add: greatest_def Lower_def)
   apply arith
   apply simp apply simp
   done
 
-text {* Interpretation unfolding @{text less}, @{text join} and @{text
+lemma carrier_int:
+  "carrier (| carrier = UNIV::int set, le = op \<le> |) = UNIV"
+  apply simp
+  done
+
+text {* Interpretation unfolding @{text lless}, @{text join} and @{text
   meet} since they have natural representations in @{typ int}. *}
 
 interpretation 
-  int [unfolded less_int join_int meet_int]:
-  total_order ["UNIV::int set" "op \<le>"] by (rule int_le_total_order)
+  int [unfolded less_int join_int meet_int carrier_int]:
+  total_order ["(| carrier = UNIV::int set, le = op \<le> |)"]
+  by (rule int_le_total_order)
 
 
 subsubsection {* Generated Ideals of @{text "\<Z>"} *}