changeset 10711 | a9f6994fb906 |
parent 10706 | f02834001fca |
child 10832 | e33b47e4246d |
--- 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];