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/ZF/Nat.ML
changeset 1956 589af052bcd4
parent 1610 60ab5844fe81
child 2033 639de962ded4 
--- a/src/ZF/Nat.ML	Thu Sep 05 18:29:43 1996 +0200
+++ b/src/ZF/Nat.ML	Thu Sep 05 18:30:13 1996 +0200
@@ -128,7 +128,7 @@
 by (nat_ind_tac "n" prems 1);
 by (ALLGOALS
     (asm_simp_tac
-     (ZF_ss addsimps (prems@distrib_rews@[le0_iff, le_succ_iff]))));
+     (ZF_ss addsimps (prems@distrib_simps@[le0_iff, le_succ_iff]))));
 qed "nat_induct_from_lemma";
 
 (*Induction starting from m rather than 0*)
isabelle