src/HOL/AxClasses/Lattice/OrdDefs.ML
changeset 2606 27cdd600a3b1
parent 1899 0075a8d26a80
child 4091 771b1f6422a8
--- a/src/HOL/AxClasses/Lattice/OrdDefs.ML	Mon Feb 10 16:16:55 1997 +0100
+++ b/src/HOL/AxClasses/Lattice/OrdDefs.ML	Wed Feb 12 15:42:31 1997 +0100
@@ -20,7 +20,7 @@
   ba 1;
 qed "le_prod_trans";
 
-goalw thy [le_prod_def] "x [= y & y [= x --> x = (y::'a::order*'b::order)";
+goalw thy [le_prod_def] "x [= y & y [= x --> x = (y::'a::partial_order*'b::partial_order)";
   by (safe_tac (!claset));
   by (stac Pair_fst_snd_eq 1);
   br conjI 1;
@@ -44,7 +44,7 @@
   by (Fast_tac 1);
 qed "le_fun_trans";
 
-goalw thy [le_fun_def] "f [= g & g [= f --> f = (g::'a=>'b::order)";
+goalw thy [le_fun_def] "f [= g & g [= f --> f = (g::'a=>'b::partial_order)";
   by (safe_tac (!claset));
   br ext 1;
   br (le_antisym RS mp) 1;
@@ -72,7 +72,7 @@
   br le_trans 1;
 qed "le_dual_trans";
 
-goalw thy [le_dual_def] "x [= y & y [= x --> x = (y::'a::order dual)";
+goalw thy [le_dual_def] "x [= y & y [= x --> x = (y::'a::partial_order dual)";
   by (safe_tac (!claset));
   br (Rep_dual_inverse RS subst) 1;
   br sym 1;
@@ -83,6 +83,6 @@
   ba 1;
 qed "le_dual_antisym";
 
-goalw thy [le_dual_def] "x [= y | y [= (x::'a::lin_order dual)";
-  br le_lin 1;
-qed "le_dual_lin";
+goalw thy [le_dual_def] "x [= y | y [= (x::'a::linear_order dual)";
+  br le_linear 1;
+qed "le_dual_linear";