src/HOL/Induct/LList.ML
changeset 3427 e7cef2081106
parent 3120 c58423c20740
child 3842 b55686a7b22c
     1.1 --- a/src/HOL/Induct/LList.ML	Fri Jun 06 13:26:41 1997 +0200
     1.2 +++ b/src/HOL/Induct/LList.ML	Fri Jun 06 13:28:40 1997 +0200
     1.3 @@ -27,7 +27,7 @@
     1.4  
     1.5  goal LList.thy "llist(A) = {Numb(0)} <+> (A <*> llist(A))";
     1.6  let val rew = rewrite_rule [NIL_def, CONS_def] in  
     1.7 -by (fast_tac (!claset addSIs (equalityI :: map rew llist.intrs)
     1.8 +by (fast_tac (!claset addSIs (map rew llist.intrs)
     1.9                        addEs [rew llist.elim]) 1)
    1.10  end;
    1.11  qed "llist_unfold";
    1.12 @@ -148,7 +148,7 @@
    1.13  (*This theorem is actually used, unlike the many similar ones in ZF*)
    1.14  goal LList.thy "LListD(r) = diag({Numb(0)}) <++> (r <**> LListD(r))";
    1.15  let val rew = rewrite_rule [NIL_def, CONS_def] in  
    1.16 -by (fast_tac (!claset addSIs (equalityI :: map rew LListD.intrs)
    1.17 +by (fast_tac (!claset addSIs (map rew LListD.intrs)
    1.18                        addEs [rew LListD.elim]) 1)
    1.19  end;
    1.20  qed "LListD_unfold";
    1.21 @@ -157,7 +157,7 @@
    1.22  by (res_inst_tac [("n", "k")] less_induct 1);
    1.23  by (safe_tac ((claset_of "Fun") delrules [equalityI]));
    1.24  by (etac LListD.elim 1);
    1.25 -by (safe_tac (((claset_of "Prod") delrules [equalityI]) addSEs [diagE]));
    1.26 +by (safe_tac (claset_of "Prod" delrules [equalityI] addSEs [diagE]));
    1.27  by (res_inst_tac [("n", "n")] natE 1);
    1.28  by (asm_simp_tac (!simpset addsimps [ntrunc_0]) 1);
    1.29  by (rename_tac "n'" 1);
    1.30 @@ -392,7 +392,7 @@
    1.31  (** Injectiveness of CONS and LCons **)
    1.32  
    1.33  goalw LList.thy [CONS_def] "(CONS M N=CONS M' N') = (M=M' & N=N')";
    1.34 -by (fast_tac (!claset addSEs [Scons_inject, make_elim In1_inject]) 1);
    1.35 +by (fast_tac (!claset addSEs [Scons_inject]) 1);
    1.36  qed "CONS_CONS_eq2";
    1.37  
    1.38  bind_thm ("CONS_inject", (CONS_CONS_eq RS iffD1 RS conjE));