# 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 **)