| changeset 8127 | 68c6159440f1 |
| parent 6153 | bff90585cce5 |
| child 9180 | 3bda56c0d70d |
--- a/src/ZF/Nat.ML Thu Jan 13 17:36:02 2000 +0100 +++ b/src/ZF/Nat.ML Thu Jan 13 17:36:58 2000 +0100 @@ -74,6 +74,8 @@ by (REPEAT (ares_tac [Ord_0, Ord_succ] 1)); qed "nat_into_Ord"; +Addsimps [nat_into_Ord]; + (* i: nat ==> 0 le i; same thing as 0<succ(i) *) bind_thm ("nat_0_le", nat_into_Ord RS Ord_0_le);