author | paulson |
Wed, 20 Dec 2000 12:14:50 +0100 | |
changeset 10711 | a9f6994fb906 |
parent 10710 | 0c8d58332658 |
child 10712 | 351ba950d4d9 |
src/HOL/NatDef.ML | file | annotate | diff | comparison | revisions |
--- a/src/HOL/NatDef.ML Wed Dec 20 12:14:26 2000 +0100 +++ b/src/HOL/NatDef.ML Wed Dec 20 12:14:50 2000 +0100 @@ -528,7 +528,8 @@ Conditional rewrite rules are tried after unconditional ones. **) -Goal "True ==> (0 = x) = (x = (0::nat))"; +(*Polymorphic, not just for "nat"*) +Goal "True ==> (0 = x) = (x = 0)"; by Auto_tac; qed "zero_reorient"; Addsimps [zero_reorient];