| changeset 11386 | cf8d81cf8034 |
| parent 9907 | 473a6604da94 |
| child 12789 | 459b5de466b2 |
--- a/src/ZF/Arith.ML Tue Jun 26 17:07:02 2001 +0200 +++ b/src/ZF/Arith.ML Tue Jun 26 17:25:41 2001 +0200 @@ -65,6 +65,10 @@ qed "natify_ident"; Addsimps [natify_ident]; +Goal "[|natify(x) = y; x: nat|] ==> x=y"; +by Auto_tac; +qed "natify_eqE"; + (*** Collapsing rules: to remove natify from arithmetic expressions ***)