src/HOL/AxClasses/Lattice/OrdDefs.ML
changeset 4153 e534c4c32d54
parent 4091 771b1f6422a8
child 5069 3ea049f7979d
     1.1 --- a/src/HOL/AxClasses/Lattice/OrdDefs.ML	Wed Nov 05 13:14:15 1997 +0100
     1.2 +++ b/src/HOL/AxClasses/Lattice/OrdDefs.ML	Wed Nov 05 13:23:46 1997 +0100
     1.3 @@ -7,47 +7,47 @@
     1.4  (* pairs *)
     1.5  
     1.6  goalw thy [le_prod_def] "x [= (x::'a::quasi_order*'b::quasi_order)";
     1.7 -  br conjI 1;
     1.8 -  br le_refl 1;
     1.9 -  br le_refl 1;
    1.10 +  by (rtac conjI 1);
    1.11 +  by (rtac le_refl 1);
    1.12 +  by (rtac le_refl 1);
    1.13  qed "le_prod_refl";
    1.14  
    1.15  goalw thy [le_prod_def] "x [= y & y [= z --> x [= (z::'a::quasi_order*'b::quasi_order)";
    1.16 -  by (safe_tac (claset()));
    1.17 -  be (conjI RS (le_trans RS mp)) 1;
    1.18 -  ba 1;
    1.19 -  be (conjI RS (le_trans RS mp)) 1;
    1.20 -  ba 1;
    1.21 +  by Safe_tac;
    1.22 +  by (etac (conjI RS (le_trans RS mp)) 1);
    1.23 +  by (assume_tac 1);
    1.24 +  by (etac (conjI RS (le_trans RS mp)) 1);
    1.25 +  by (assume_tac 1);
    1.26  qed "le_prod_trans";
    1.27  
    1.28  goalw thy [le_prod_def] "x [= y & y [= x --> x = (y::'a::partial_order*'b::partial_order)";
    1.29 -  by (safe_tac (claset()));
    1.30 +  by Safe_tac;
    1.31    by (stac Pair_fst_snd_eq 1);
    1.32 -  br conjI 1;
    1.33 -  be (conjI RS (le_antisym RS mp)) 1;
    1.34 -  ba 1;
    1.35 -  be (conjI RS (le_antisym RS mp)) 1;
    1.36 -  ba 1;
    1.37 +  by (rtac conjI 1);
    1.38 +  by (etac (conjI RS (le_antisym RS mp)) 1);
    1.39 +  by (assume_tac 1);
    1.40 +  by (etac (conjI RS (le_antisym RS mp)) 1);
    1.41 +  by (assume_tac 1);
    1.42  qed "le_prod_antisym";
    1.43  
    1.44  
    1.45  (* functions *)
    1.46  
    1.47  goalw thy [le_fun_def] "f [= (f::'a=>'b::quasi_order)";
    1.48 -  br allI 1;
    1.49 -  br le_refl 1;
    1.50 +  by (rtac allI 1);
    1.51 +  by (rtac le_refl 1);
    1.52  qed "le_fun_refl";
    1.53  
    1.54  goalw thy [le_fun_def] "f [= g & g [= h --> f [= (h::'a=>'b::quasi_order)";
    1.55 -  by (safe_tac (claset()));
    1.56 -  br (le_trans RS mp) 1;
    1.57 +  by Safe_tac;
    1.58 +  by (rtac (le_trans RS mp) 1);
    1.59    by (Fast_tac 1);
    1.60  qed "le_fun_trans";
    1.61  
    1.62  goalw thy [le_fun_def] "f [= g & g [= f --> f = (g::'a=>'b::partial_order)";
    1.63 -  by (safe_tac (claset()));
    1.64 -  br ext 1;
    1.65 -  br (le_antisym RS mp) 1;
    1.66 +  by Safe_tac;
    1.67 +  by (rtac ext 1);
    1.68 +  by (rtac (le_antisym RS mp) 1);
    1.69    by (Fast_tac 1);
    1.70  qed "le_fun_antisym";
    1.71  
    1.72 @@ -57,32 +57,32 @@
    1.73  
    1.74  (*"'a dual" is even an isotype*)
    1.75  goal thy "Rep_dual (Abs_dual y) = y";
    1.76 -  br Abs_dual_inverse 1;
    1.77 +  by (rtac Abs_dual_inverse 1);
    1.78    by (rewtac dual_def);
    1.79    by (Fast_tac 1);
    1.80  qed "Abs_dual_inverse'";
    1.81  
    1.82  
    1.83  goalw thy [le_dual_def] "x [= (x::'a::quasi_order dual)";
    1.84 -  br le_refl 1;
    1.85 +  by (rtac le_refl 1);
    1.86  qed "le_dual_refl";
    1.87  
    1.88  goalw thy [le_dual_def] "x [= y & y [= z --> x [= (z::'a::quasi_order dual)";
    1.89    by (stac conj_commut 1);
    1.90 -  br le_trans 1;
    1.91 +  by (rtac le_trans 1);
    1.92  qed "le_dual_trans";
    1.93  
    1.94  goalw thy [le_dual_def] "x [= y & y [= x --> x = (y::'a::partial_order dual)";
    1.95 -  by (safe_tac (claset()));
    1.96 -  br (Rep_dual_inverse RS subst) 1;
    1.97 -  br sym 1;
    1.98 -  br (Rep_dual_inverse RS subst) 1;
    1.99 -  br arg_cong 1;
   1.100 +  by Safe_tac;
   1.101 +  by (rtac (Rep_dual_inverse RS subst) 1);
   1.102 +  by (rtac sym 1);
   1.103 +  by (rtac (Rep_dual_inverse RS subst) 1);
   1.104 +  by (rtac arg_cong 1);
   1.105    back();
   1.106 -  be (conjI RS (le_antisym RS mp)) 1;
   1.107 -  ba 1;
   1.108 +  by (etac (conjI RS (le_antisym RS mp)) 1);
   1.109 +  by (assume_tac 1);
   1.110  qed "le_dual_antisym";
   1.111  
   1.112  goalw thy [le_dual_def] "x [= y | y [= (x::'a::linear_order dual)";
   1.113 -  br le_linear 1;
   1.114 +  by (rtac le_linear 1);
   1.115  qed "le_dual_linear";