src/HOL/AxClasses/Lattice/LatPreInsts.ML
changeset 4091 771b1f6422a8
parent 1899 0075a8d26a80
child 4153 e534c4c32d54
     1.1 --- a/src/HOL/AxClasses/Lattice/LatPreInsts.ML	Mon Nov 03 12:22:43 1997 +0100
     1.2 +++ b/src/HOL/AxClasses/Lattice/LatPreInsts.ML	Mon Nov 03 12:24:13 1997 +0100
     1.3 @@ -22,13 +22,13 @@
     1.4  
     1.5  goalw thy [is_inf_def, le_prod_def] "is_inf p q (fst p && fst q, snd p && snd q)";
     1.6    by (Simp_tac 1);
     1.7 -  by (safe_tac (!claset));
     1.8 +  by (safe_tac (claset()));
     1.9    by (REPEAT_FIRST (fn i => resolve_tac [inf_lb1, inf_lb2, inf_ub_lbs] i ORELSE atac i));
    1.10  qed "prod_is_inf";
    1.11  
    1.12  goalw thy [is_sup_def, le_prod_def] "is_sup p q (fst p || fst q, snd p || snd q)";
    1.13    by (Simp_tac 1);
    1.14 -  by (safe_tac (!claset));
    1.15 +  by (safe_tac (claset()));
    1.16    by (REPEAT_FIRST (fn i => resolve_tac [sup_ub1, sup_ub2, sup_lb_ubs] i ORELSE atac i));
    1.17  qed "prod_is_sup";
    1.18  
    1.19 @@ -36,7 +36,7 @@
    1.20  (* functions *)
    1.21  
    1.22  goalw thy [is_inf_def, le_fun_def] "is_inf f g (%x. f x && g x)";
    1.23 -  by (safe_tac (!claset));
    1.24 +  by (safe_tac (claset()));
    1.25    br inf_lb1 1;
    1.26    br inf_lb2 1;
    1.27    br inf_ub_lbs 1;
    1.28 @@ -44,7 +44,7 @@
    1.29  qed "fun_is_inf";
    1.30  
    1.31  goalw thy [is_sup_def, le_fun_def] "is_sup f g (%x. f x || g x)";
    1.32 -  by (safe_tac (!claset));
    1.33 +  by (safe_tac (claset()));
    1.34    br sup_ub1 1;
    1.35    br sup_ub2 1;
    1.36    br sup_lb_ubs 1;
    1.37 @@ -57,7 +57,7 @@
    1.38  
    1.39  goalw thy [is_inf_def, le_dual_def] "is_inf x y (Abs_dual (Rep_dual x || Rep_dual y))";
    1.40    by (stac Abs_dual_inverse' 1);
    1.41 -  by (safe_tac (!claset));
    1.42 +  by (safe_tac (claset()));
    1.43    br sup_ub1 1;
    1.44    br sup_ub2 1;
    1.45    br sup_lb_ubs 1;
    1.46 @@ -67,7 +67,7 @@
    1.47  
    1.48  goalw thy [is_sup_def, le_dual_def] "is_sup x y (Abs_dual (Rep_dual x && Rep_dual y))";
    1.49    by (stac Abs_dual_inverse' 1);
    1.50 -  by (safe_tac (!claset));
    1.51 +  by (safe_tac (claset()));
    1.52    br inf_lb1 1;
    1.53    br inf_lb2 1;
    1.54    br inf_ub_lbs 1;