1.1 --- a/src/HOL/AxClasses/Lattice/OrdDefs.ML	Mon Feb 10 16:16:55 1997 +0100
     1.2 +++ b/src/HOL/AxClasses/Lattice/OrdDefs.ML	Wed Feb 12 15:42:31 1997 +0100
     1.3 @@ -20,7 +20,7 @@
     1.4    ba 1;
     1.5  qed "le_prod_trans";
     1.6  
     1.7 -goalw thy [le_prod_def] "x [= y & y [= x --> x = (y::'a::order*'b::order)";
     1.8 +goalw thy [le_prod_def] "x [= y & y [= x --> x = (y::'a::partial_order*'b::partial_order)";
     1.9    by (safe_tac (!claset));
    1.10    by (stac Pair_fst_snd_eq 1);
    1.11    br conjI 1;
    1.12 @@ -44,7 +44,7 @@
    1.13    by (Fast_tac 1);
    1.14  qed "le_fun_trans";
    1.15  
    1.16 -goalw thy [le_fun_def] "f [= g & g [= f --> f = (g::'a=>'b::order)";
    1.17 +goalw thy [le_fun_def] "f [= g & g [= f --> f = (g::'a=>'b::partial_order)";
    1.18    by (safe_tac (!claset));
    1.19    br ext 1;
    1.20    br (le_antisym RS mp) 1;
    1.21 @@ -72,7 +72,7 @@
    1.22    br le_trans 1;
    1.23  qed "le_dual_trans";
    1.24  
    1.25 -goalw thy [le_dual_def] "x [= y & y [= x --> x = (y::'a::order dual)";
    1.26 +goalw thy [le_dual_def] "x [= y & y [= x --> x = (y::'a::partial_order dual)";
    1.27    by (safe_tac (!claset));
    1.28    br (Rep_dual_inverse RS subst) 1;
    1.29    br sym 1;
    1.30 @@ -83,6 +83,6 @@
    1.31    ba 1;
    1.32  qed "le_dual_antisym";
    1.33  
    1.34 -goalw thy [le_dual_def] "x [= y | y [= (x::'a::lin_order dual)";
    1.35 -  br le_lin 1;
    1.36 -qed "le_dual_lin";
    1.37 +goalw thy [le_dual_def] "x [= y | y [= (x::'a::linear_order dual)";
    1.38 +  br le_linear 1;
    1.39 +qed "le_dual_linear";