author | paulson |
Wed, 27 Apr 2005 16:39:59 +0200 | |
changeset 15861 | cf2c6cf35216 |
parent 15860 | a344c4284972 |
child 15862 | 67574c1b15a0 |
--- a/src/HOL/NatArith.thy Wed Apr 27 16:39:44 2005 +0200 +++ b/src/HOL/NatArith.thy Wed Apr 27 16:39:59 2005 +0200 @@ -132,8 +132,6 @@ ML {* -val nat_diff_split = thm "nat_diff_split"; -val nat_diff_split_asm = thm "nat_diff_split_asm"; val pred_nat_trancl_eq_le = thm "pred_nat_trancl_eq_le"; val nat_diff_split = thm "nat_diff_split"; val nat_diff_split_asm = thm "nat_diff_split_asm";