--- 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";