src/HOL/Hoare/List_Examples.ML
changeset 4153 e534c4c32d54
parent 4089 96fba19bcbe2
child 4724 3d2375efb80e
     1.1 --- a/src/HOL/Hoare/List_Examples.ML	Wed Nov 05 13:14:15 1997 +0100
     1.2 +++ b/src/HOL/Hoare/List_Examples.ML	Wed Nov 05 13:23:46 1997 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4  \{y=rev(X)}";
     1.5  by (hoare_tac 1);
     1.6  by (asm_full_simp_tac (simpset() addsimps [neq_Nil_conv]) 1);
     1.7 -by (safe_tac (claset()));
     1.8 +by Safe_tac;
     1.9  by (Asm_full_simp_tac 1);
    1.10  by (Asm_full_simp_tac 1);
    1.11  qed "imperative_reverse";
    1.12 @@ -23,7 +23,7 @@
    1.13  \{y = X@Y}";
    1.14  by (hoare_tac 1);
    1.15  by (asm_full_simp_tac (simpset() addsimps [neq_Nil_conv]) 1);
    1.16 -by (safe_tac (claset()));
    1.17 +by Safe_tac;
    1.18  by (Asm_full_simp_tac 1);
    1.19  by (Asm_full_simp_tac 1);
    1.20  qed "imperative_append";