src/ZF/Ord.ML
changeset 6 8ce8c4d13d4d
parent 0 a5a9c433f639
child 15 6c6d2f6e3185
     1.1 --- a/src/ZF/Ord.ML	Fri Sep 17 12:53:53 1993 +0200
     1.2 +++ b/src/ZF/Ord.ML	Fri Sep 17 16:16:38 1993 +0200
     1.3 @@ -318,7 +318,7 @@
     1.4  
     1.5  goal Ord.thy
     1.6      "!!i j. [| Ord(i);  Ord(j) |] ==> i<=succ(j) <-> i<=j | i=succ(j)";
     1.7 -by (ASM_SIMP_TAC (ZF_ss addrews [member_succ_iff RS iff_sym, Ord_succ]) 1);
     1.8 +by (asm_simp_tac (ZF_ss addsimps [member_succ_iff RS iff_sym, Ord_succ]) 1);
     1.9  by (fast_tac ZF_cs 1);
    1.10  val subset_succ_iff = result();
    1.11  
    1.12 @@ -356,17 +356,17 @@
    1.13  goal Ord.thy "!!i j k. [| i:k;  j:k;  Ord(k) |] ==> i Un j : k";
    1.14  by (res_inst_tac [("i","i"),("j","j")] Ord_subset 1);
    1.15  by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 1));
    1.16 -by (ASM_SIMP_TAC (ZF_ss addrews [subset_Un_iff RS iffD1]) 1);
    1.17 +by (asm_simp_tac (ZF_ss addsimps [subset_Un_iff RS iffD1]) 1);
    1.18  by (rtac (Un_commute RS ssubst) 1);
    1.19 -by (ASM_SIMP_TAC (ZF_ss addrews [subset_Un_iff RS iffD1]) 1);
    1.20 +by (asm_simp_tac (ZF_ss addsimps [subset_Un_iff RS iffD1]) 1);
    1.21  val Ord_member_UnI = result();
    1.22  
    1.23  goal Ord.thy "!!i j k. [| i:k;  j:k;  Ord(k) |] ==> i Int j : k";
    1.24  by (res_inst_tac [("i","i"),("j","j")] Ord_subset 1);
    1.25  by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 1));
    1.26 -by (ASM_SIMP_TAC (ZF_ss addrews [subset_Int_iff RS iffD1]) 1);
    1.27 +by (asm_simp_tac (ZF_ss addsimps [subset_Int_iff RS iffD1]) 1);
    1.28  by (rtac (Int_commute RS ssubst) 1);
    1.29 -by (ASM_SIMP_TAC (ZF_ss addrews [subset_Int_iff RS iffD1]) 1);
    1.30 +by (asm_simp_tac (ZF_ss addsimps [subset_Int_iff RS iffD1]) 1);
    1.31  val Ord_member_IntI = result();
    1.32  
    1.33