src/HOL/AxClasses/Lattice/LatInsts.ML
changeset 4153 e534c4c32d54
parent 4091 771b1f6422a8
child 5069 3ea049f7979d
     1.1 --- a/src/HOL/AxClasses/Lattice/LatInsts.ML	Wed Nov 05 13:14:15 1997 +0100
     1.2 +++ b/src/HOL/AxClasses/Lattice/LatInsts.ML	Wed Nov 05 13:23:46 1997 +0100
     1.3 @@ -3,15 +3,15 @@
     1.4  
     1.5  
     1.6  goal thy "Inf {x, y} = x && y";
     1.7 -  br (Inf_uniq RS mp) 1;
     1.8 +  by (rtac (Inf_uniq RS mp) 1);
     1.9    by (stac bin_is_Inf_eq 1);
    1.10 -  br inf_is_inf 1;
    1.11 +  by (rtac inf_is_inf 1);
    1.12  qed "bin_Inf_eq";
    1.13  
    1.14  goal thy "Sup {x, y} = x || y";
    1.15 -  br (Sup_uniq RS mp) 1;
    1.16 +  by (rtac (Sup_uniq RS mp) 1);
    1.17    by (stac bin_is_Sup_eq 1);
    1.18 -  br sup_is_sup 1;
    1.19 +  by (rtac sup_is_sup 1);
    1.20  qed "bin_Sup_eq";
    1.21  
    1.22  
    1.23 @@ -19,39 +19,39 @@
    1.24  (* Unions and limits *)
    1.25  
    1.26  goal thy "Inf (A Un B) = Inf A && Inf B";
    1.27 -  br (Inf_uniq RS mp) 1;
    1.28 +  by (rtac (Inf_uniq RS mp) 1);
    1.29    by (rewtac is_Inf_def);
    1.30 -  by (safe_tac (claset()));
    1.31 +  by Safe_tac;
    1.32  
    1.33 -  br (conjI RS (le_trans RS mp)) 1;
    1.34 -  br inf_lb1 1;
    1.35 -  be Inf_lb 1;
    1.36 +  by (rtac (conjI RS (le_trans RS mp)) 1);
    1.37 +  by (rtac inf_lb1 1);
    1.38 +  by (etac Inf_lb 1);
    1.39  
    1.40 -  br (conjI RS (le_trans RS mp)) 1;
    1.41 -  br inf_lb2 1;
    1.42 -  be Inf_lb 1;
    1.43 +  by (rtac (conjI RS (le_trans RS mp)) 1);
    1.44 +  by (rtac inf_lb2 1);
    1.45 +  by (etac Inf_lb 1);
    1.46  
    1.47    by (stac le_inf_eq 1);
    1.48 -  br conjI 1;
    1.49 -  br Inf_ub_lbs 1;
    1.50 +  by (rtac conjI 1);
    1.51 +  by (rtac Inf_ub_lbs 1);
    1.52    by (Fast_tac 1);
    1.53 -  br Inf_ub_lbs 1;
    1.54 +  by (rtac Inf_ub_lbs 1);
    1.55    by (Fast_tac 1);
    1.56  qed "Inf_Un_eq";
    1.57  
    1.58  goal thy "Inf (UN i:A. B i) = Inf {Inf (B i) |i. i:A}";
    1.59 -  br (Inf_uniq RS mp) 1;
    1.60 +  by (rtac (Inf_uniq RS mp) 1);
    1.61    by (rewtac is_Inf_def);
    1.62 -  by (safe_tac (claset()));
    1.63 +  by Safe_tac;
    1.64    (*level 3*)
    1.65 -  br (conjI RS (le_trans RS mp)) 1;
    1.66 -  be Inf_lb 2;
    1.67 -  br (sing_Inf_eq RS subst) 1;
    1.68 -  br (Inf_subset_antimon RS mp) 1;
    1.69 +  by (rtac (conjI RS (le_trans RS mp)) 1);
    1.70 +  by (etac Inf_lb 2);
    1.71 +  by (rtac (sing_Inf_eq RS subst) 1);
    1.72 +  by (rtac (Inf_subset_antimon RS mp) 1);
    1.73    by (Fast_tac 1);
    1.74    (*level 8*)
    1.75    by (stac le_Inf_eq 1);
    1.76 -  by (safe_tac (claset()));
    1.77 +  by Safe_tac;
    1.78    by (stac le_Inf_eq 1);
    1.79    by (Fast_tac 1);
    1.80  qed "Inf_UN_eq";
    1.81 @@ -59,40 +59,40 @@
    1.82  
    1.83  
    1.84  goal thy "Sup (A Un B) = Sup A || Sup B";
    1.85 -  br (Sup_uniq RS mp) 1;
    1.86 +  by (rtac (Sup_uniq RS mp) 1);
    1.87    by (rewtac is_Sup_def);
    1.88 -  by (safe_tac (claset()));
    1.89 +  by Safe_tac;
    1.90  
    1.91 -  br (conjI RS (le_trans RS mp)) 1;
    1.92 -  be Sup_ub 1;
    1.93 -  br sup_ub1 1;
    1.94 +  by (rtac (conjI RS (le_trans RS mp)) 1);
    1.95 +  by (etac Sup_ub 1);
    1.96 +  by (rtac sup_ub1 1);
    1.97  
    1.98 -  br (conjI RS (le_trans RS mp)) 1;
    1.99 -  be Sup_ub 1;
   1.100 -  br sup_ub2 1;
   1.101 +  by (rtac (conjI RS (le_trans RS mp)) 1);
   1.102 +  by (etac Sup_ub 1);
   1.103 +  by (rtac sup_ub2 1);
   1.104  
   1.105    by (stac ge_sup_eq 1);
   1.106 -  br conjI 1;
   1.107 -  br Sup_lb_ubs 1;
   1.108 +  by (rtac conjI 1);
   1.109 +  by (rtac Sup_lb_ubs 1);
   1.110    by (Fast_tac 1);
   1.111 -  br Sup_lb_ubs 1;
   1.112 +  by (rtac Sup_lb_ubs 1);
   1.113    by (Fast_tac 1);
   1.114  qed "Sup_Un_eq";
   1.115  
   1.116  goal thy "Sup (UN i:A. B i) = Sup {Sup (B i) |i. i:A}";
   1.117 -  br (Sup_uniq RS mp) 1;
   1.118 +  by (rtac (Sup_uniq RS mp) 1);
   1.119    by (rewtac is_Sup_def);
   1.120 -  by (safe_tac (claset()));
   1.121 +  by Safe_tac;
   1.122    (*level 3*)
   1.123 -  br (conjI RS (le_trans RS mp)) 1;
   1.124 -  be Sup_ub 1;
   1.125 -  br (sing_Sup_eq RS subst) 1;
   1.126 +  by (rtac (conjI RS (le_trans RS mp)) 1);
   1.127 +  by (etac Sup_ub 1);
   1.128 +  by (rtac (sing_Sup_eq RS subst) 1);
   1.129    back();
   1.130 -  br (Sup_subset_mon RS mp) 1;
   1.131 +  by (rtac (Sup_subset_mon RS mp) 1);
   1.132    by (Fast_tac 1);
   1.133    (*level 8*)
   1.134    by (stac ge_Sup_eq 1);
   1.135 -  by (safe_tac (claset()));
   1.136 +  by Safe_tac;
   1.137    by (stac ge_Sup_eq 1);
   1.138    by (Fast_tac 1);
   1.139  qed "Sup_UN_eq";