src/HOL/Datatype_Universe.ML
changeset 10908 a7cfffb5d7dc
parent 10850 e1a793957a8f
child 11464 ddea204de5bc
     1.1 --- a/src/HOL/Datatype_Universe.ML	Tue Jan 16 00:29:12 2001 +0100
     1.2 +++ b/src/HOL/Datatype_Universe.ML	Tue Jan 16 00:29:43 2001 +0100
     1.3 @@ -7,7 +7,7 @@
     1.4  (** apfst -- can be used in similar type definitions **)
     1.5  
     1.6  Goalw [apfst_def] "apfst f (a,b) = (f(a),b)";
     1.7 -by (rtac split 1);
     1.8 +by (rtac split_conv 1);
     1.9  qed "apfst_conv";
    1.10  
    1.11  val [major,minor] = Goal
    1.12 @@ -61,7 +61,7 @@
    1.13  by (etac Abs_Node_inverse 1);
    1.14  qed "inj_on_Abs_Node";
    1.15  
    1.16 -bind_thm ("Abs_Node_inject", inj_on_Abs_Node RS inj_onD);
    1.17 +bind_thm ("Abs_Node_inj", inj_on_Abs_Node RS inj_onD);
    1.18  
    1.19  
    1.20  (*** Introduction rules for Node ***)
    1.21 @@ -84,7 +84,7 @@
    1.22  by (rtac notI 1);
    1.23  by (etac (equalityD2 RS subsetD RS UnE) 1);
    1.24  by (rtac singletonI 1);
    1.25 -by (REPEAT (eresolve_tac [imageE, Abs_Node_inject RS apfst_convE, 
    1.26 +by (REPEAT (eresolve_tac [imageE, Abs_Node_inj RS apfst_convE, 
    1.27                            Pair_inject, sym RS Push_neq_K0] 1
    1.28       ORELSE resolve_tac [Node_K0_I, Rep_Node RS Node_Push_I] 1));
    1.29  qed "Scons_not_Atom";
    1.30 @@ -96,7 +96,7 @@
    1.31  (** Atomic nodes **)
    1.32  
    1.33  Goalw [Atom_def] "inj(Atom)";
    1.34 -by (blast_tac (claset() addSIs [injI, Node_K0_I] addSDs [Abs_Node_inject]) 1);
    1.35 +by (blast_tac (claset() addSIs [injI, Node_K0_I] addSDs [Abs_Node_inj]) 1);
    1.36  qed "inj_Atom";
    1.37  bind_thm ("Atom_inject", inj_Atom RS injD);
    1.38  
    1.39 @@ -126,7 +126,7 @@
    1.40  val [major,minor] = Goalw [Push_Node_def]
    1.41      "[| Push_Node i m =Push_Node j n;  [| i=j;  m=n |] ==> P \
    1.42  \    |] ==> P";
    1.43 -by (rtac (major RS Abs_Node_inject RS apfst_convE) 1);
    1.44 +by (rtac (major RS Abs_Node_inj RS apfst_convE) 1);
    1.45  by (REPEAT (resolve_tac [Rep_Node RS Node_Push_I] 1));
    1.46  by (etac (sym RS apfst_convE) 1);
    1.47  by (rtac minor 1);
    1.48 @@ -207,7 +207,7 @@
    1.49  
    1.50  
    1.51  Goalw [ndepth_def] "ndepth (Abs_Node(%k. Inr 0, x)) = 0";
    1.52 -by (EVERY1[stac (Node_K0_I RS Abs_Node_inverse), stac split]);
    1.53 +by (EVERY1[stac (Node_K0_I RS Abs_Node_inverse), stac split_conv]);
    1.54  by (rtac Least_equality 1);
    1.55  by Auto_tac;  
    1.56  qed "ndepth_K0";