diff -r 197e5a88c9df -r da61bfa0a391 src/ZF/Nat.thy
--- a/src/ZF/Nat.thy	Tue May 28 11:06:55 2002 +0200
+++ b/src/ZF/Nat.thy	Tue May 28 11:07:36 2002 +0200
@@ -299,10 +299,8 @@
 val lt_nat_in_nat = thm "lt_nat_in_nat";
 val le_in_nat = thm "le_in_nat";
 val complete_induct = thm "complete_induct";
-val nat_induct_from_lemma = thm "nat_induct_from_lemma";
 val nat_induct_from = thm "nat_induct_from";
 val diff_induct = thm "diff_induct";
-val succ_lt_induct_lemma = thm "succ_lt_induct_lemma";
 val succ_lt_induct = thm "succ_lt_induct";
 val nat_case_0 = thm "nat_case_0";
 val nat_case_succ = thm "nat_case_succ";