Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/NatDef.ML
changeset 4153 e534c4c32d54
parent 4104 84433b1ab826
child 4356 0dfd34f0d33d 
--- a/src/HOL/NatDef.ML	Wed Nov 05 13:14:15 1997 +0100
+++ b/src/HOL/NatDef.ML	Wed Nov 05 13:23:46 1997 +0100
@@ -628,11 +628,11 @@
         hyp_subst_tac 1,
         rewtac Least_nat_def,
         rtac (select_equality RS arg_cong RS sym) 1,
-        safe_tac (claset()),
+        Safe_tac,
         dtac Suc_mono 1,
         Blast_tac 1,
         cut_facts_tac [less_linear] 1,
-        safe_tac (claset()),
+        Safe_tac,
         atac 2,
         Blast_tac 2,
         dtac Suc_mono 1,
isabelle