deleted obsolete theorems
authorpaulson
Mon, 22 Jan 2001 11:45:57 +0100
changeset 10960 50b57b373d79
parent 10959 64c26f326743
child 10961 74817560a8e8
deleted obsolete theorems
src/HOL/Integ/nat_bin.ML
--- a/src/HOL/Integ/nat_bin.ML	Mon Jan 22 11:45:29 2001 +0100
+++ b/src/HOL/Integ/nat_bin.ML	Mon Jan 22 11:45:57 2001 +0100
@@ -361,8 +361,6 @@
 bind_thm ("zero_induct'", rename_numerals zero_induct);
 bind_thm ("diff_self_eq_0'", rename_numerals diff_self_eq_0);
 bind_thm ("mult_eq_self_implies_10'", rename_numerals mult_eq_self_implies_10);
-bind_thm ("le_pred_eq'", rename_numerals le_pred_eq);
-bind_thm ("less_pred_eq'", rename_numerals less_pred_eq);
 
 (** Divides **)