src/HOL/AxClasses/Lattice/LatPreInsts.ML
changeset 1899 0075a8d26a80
parent 1573 6d66b59f94a9
child 4091 771b1f6422a8
     1.1 --- a/src/HOL/AxClasses/Lattice/LatPreInsts.ML	Fri Aug 02 12:16:11 1996 +0200
     1.2 +++ b/src/HOL/AxClasses/Lattice/LatPreInsts.ML	Fri Aug 02 12:25:26 1996 +0200
     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 HOL_cs);
     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 HOL_cs);
    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,19 +36,19 @@
    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 HOL_cs);
    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 -  by (REPEAT_FIRST (fast_tac HOL_cs));
    1.29 +  by (REPEAT_FIRST (Fast_tac));
    1.30  qed "fun_is_inf";
    1.31  
    1.32  goalw thy [is_sup_def, le_fun_def] "is_sup f g (%x. f x || g x)";
    1.33 -  by (safe_tac HOL_cs);
    1.34 +  by (safe_tac (!claset));
    1.35    br sup_ub1 1;
    1.36    br sup_ub2 1;
    1.37    br sup_lb_ubs 1;
    1.38 -  by (REPEAT_FIRST (fast_tac HOL_cs));
    1.39 +  by (REPEAT_FIRST (Fast_tac));
    1.40  qed "fun_is_sup";
    1.41  
    1.42  
    1.43 @@ -57,7 +57,7 @@
    1.44  
    1.45  goalw thy [is_inf_def, le_dual_def] "is_inf x y (Abs_dual (Rep_dual x || Rep_dual y))";
    1.46    by (stac Abs_dual_inverse' 1);
    1.47 -  by (safe_tac HOL_cs);
    1.48 +  by (safe_tac (!claset));
    1.49    br sup_ub1 1;
    1.50    br sup_ub2 1;
    1.51    br sup_lb_ubs 1;
    1.52 @@ -67,7 +67,7 @@
    1.53  
    1.54  goalw thy [is_sup_def, le_dual_def] "is_sup x y (Abs_dual (Rep_dual x && Rep_dual y))";
    1.55    by (stac Abs_dual_inverse' 1);
    1.56 -  by (safe_tac HOL_cs);
    1.57 +  by (safe_tac (!claset));
    1.58    br inf_lb1 1;
    1.59    br inf_lb2 1;
    1.60    br inf_ub_lbs 1;