src/HOL/NatDef.ML
changeset 4153 e534c4c32d54
parent 4104 84433b1ab826
child 4356 0dfd34f0d33d
     1.1 --- a/src/HOL/NatDef.ML	Wed Nov 05 13:14:15 1997 +0100
     1.2 +++ b/src/HOL/NatDef.ML	Wed Nov 05 13:23:46 1997 +0100
     1.3 @@ -628,11 +628,11 @@
     1.4          hyp_subst_tac 1,
     1.5          rewtac Least_nat_def,
     1.6          rtac (select_equality RS arg_cong RS sym) 1,
     1.7 -        safe_tac (claset()),
     1.8 +        Safe_tac,
     1.9          dtac Suc_mono 1,
    1.10          Blast_tac 1,
    1.11          cut_facts_tac [less_linear] 1,
    1.12 -        safe_tac (claset()),
    1.13 +        Safe_tac,
    1.14          atac 2,
    1.15          Blast_tac 2,
    1.16          dtac Suc_mono 1,