# HG changeset patch
# User paulson
# Date 980160357 -3600
# Node ID 50b57b373d795f5f589d00a1be60017efaec2cbe
# Parent  64c26f32674312f1d626e284771a8bf55f39d0b0
deleted obsolete theorems

diff -r 64c26f326743 -r 50b57b373d79 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 **)