| changeset 15861 | cf2c6cf35216 |
| parent 15539 | 333a88244569 |
| child 16417 | 9bc16273c2d4 |
--- 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";