src/ZF/List.ML
changeset 6 8ce8c4d13d4d
parent 0 a5a9c433f639
child 15 6c6d2f6e3185
     1.1 --- a/src/ZF/List.ML	Fri Sep 17 12:53:53 1993 +0200
     1.2 +++ b/src/ZF/List.ML	Fri Sep 17 16:16:38 1993 +0200
     1.3 @@ -62,7 +62,7 @@
     1.4  \       !!x y. [| x: A;  y: list(A) |] ==> h(x,y): C(<x,y>)  \
     1.5  \    |] ==> list_case(l,c,h) : C(l)";
     1.6  by (rtac (major RS list_induct) 1);
     1.7 -by (ALLGOALS (ASM_SIMP_TAC (ZF_ss addrews
     1.8 +by (ALLGOALS (asm_simp_tac (ZF_ss addsimps
     1.9  			    ([list_case_0,list_case_Pair]@prems))));
    1.10  val list_case_type = result();
    1.11  ****)
    1.12 @@ -71,10 +71,10 @@
    1.13  (** For recursion **)
    1.14  
    1.15  goalw List.thy List.con_defs "rank(a) : rank(Cons(a,l))";
    1.16 -by (SIMP_TAC rank_ss 1);
    1.17 +by (simp_tac rank_ss 1);
    1.18  val rank_Cons1 = result();
    1.19  
    1.20  goalw List.thy List.con_defs "rank(l) : rank(Cons(a,l))";
    1.21 -by (SIMP_TAC rank_ss 1);
    1.22 +by (simp_tac rank_ss 1);
    1.23  val rank_Cons2 = result();
    1.24