--- 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";