src/CCL/Type.ML
changeset 642 0db578095e6a
parent 289 78541329ff35
child 757 2ca12511676d
     1.1 --- a/src/CCL/Type.ML	Wed Oct 12 16:38:58 1994 +0100
     1.2 +++ b/src/CCL/Type.ML	Wed Oct 19 09:23:56 1994 +0100
     1.3 @@ -67,7 +67,7 @@
     1.4                         (REPEAT_SOME (eresolve_tac (crls @ [exE,bexE,conjE,disjE]))),
     1.5                         (ALLGOALS (asm_simp_tac term_ss)),
     1.6                         (ALLGOALS (ares_tac (prems RL [lemma]) ORELSE' 
     1.7 -                                  eresolve_tac [bspec])),
     1.8 +                                  etac bspec )),
     1.9                         (safe_tac (ccl_cs addSIs prems))]);
    1.10  end;
    1.11  
    1.12 @@ -118,13 +118,13 @@
    1.13  
    1.14  val major::prems = goal Type.thy
    1.15      "mono(%X.A(X)) ==> mono(%X.[A(X)])";
    1.16 -br (subsetI RS monoI) 1;
    1.17 -bd (LiftXH RS iffD1) 1;
    1.18 -be disjE 1;
    1.19 -be (disjI1 RS (LiftXH RS iffD2)) 1;
    1.20 -br (disjI2 RS (LiftXH RS iffD2)) 1;
    1.21 -be (major RS monoD RS subsetD) 1;
    1.22 -ba 1;
    1.23 +by (rtac (subsetI RS monoI) 1);
    1.24 +by (dtac (LiftXH RS iffD1) 1);
    1.25 +by (etac disjE 1);
    1.26 +by (etac (disjI1 RS (LiftXH RS iffD2)) 1);
    1.27 +by (rtac (disjI2 RS (LiftXH RS iffD2)) 1);
    1.28 +by (etac (major RS monoD RS subsetD) 1);
    1.29 +by (assume_tac 1);
    1.30  val LiftM = result();
    1.31  
    1.32  val prems = goal Type.thy
    1.33 @@ -261,8 +261,8 @@
    1.34  val [major,minor] = goal Type.thy
    1.35      "[| <a,b> : Sigma(A,B);  [| a:A;  b:B(a) |] ==> P   \
    1.36  \    |] ==> P";
    1.37 -br (major RS (XH_to_E SgXH)) 1;
    1.38 -br minor 1;
    1.39 +by (rtac (major RS (XH_to_E SgXH)) 1);
    1.40 +by (rtac minor 1);
    1.41  by (ALLGOALS (fast_tac term_cs));
    1.42  val SgE2 = result();
    1.43  
    1.44 @@ -277,15 +277,15 @@
    1.45  (*** Infinite Data Types ***)
    1.46  
    1.47  val [mono] = goal Type.thy "mono(f) ==> lfp(f) <= gfp(f)";
    1.48 -br (lfp_lowerbound RS subset_trans) 1;
    1.49 -br (mono RS gfp_lemma3) 1;
    1.50 -br subset_refl 1;
    1.51 +by (rtac (lfp_lowerbound RS subset_trans) 1);
    1.52 +by (rtac (mono RS gfp_lemma3) 1);
    1.53 +by (rtac subset_refl 1);
    1.54  val lfp_subset_gfp = result();
    1.55  
    1.56  val prems = goal Type.thy
    1.57      "[| a:A;  !!x X.[| x:A;  ALL y:A.t(y):X |] ==> t(x) : B(X) |] ==> \
    1.58  \    t(a) : gfp(B)";
    1.59 -br coinduct 1;
    1.60 +by (rtac coinduct 1);
    1.61  by (res_inst_tac [("P","%x.EX y:A.x=t(y)")] CollectI 1);
    1.62  by (ALLGOALS (fast_tac (ccl_cs addSIs prems)));
    1.63  val gfpI = result();
    1.64 @@ -302,7 +302,7 @@
    1.65  val prems = goal Type.thy 
    1.66      "letrec g x be zero$g(x) in g(bot) : Lists(Nat)";
    1.67  by (rtac (refl RS (XH_to_I UnitXH) RS (Lists_def RS def_gfpI)) 1);
    1.68 -br (letrecB RS ssubst) 1;
    1.69 -bw cons_def;
    1.70 +by (rtac (letrecB RS ssubst) 1);
    1.71 +by (rewtac cons_def);
    1.72  by (fast_tac type_cs 1);
    1.73  result();