# HG changeset patch
# User paulson
# Date 977310890 -3600
# Node ID a9f6994fb90665321f431da9cc319c4732fd81c6
# Parent  0c8d583326587f066ec0f7d5a4851a15e77c0507
generalized the re-orientation 0f 0=... to all types

diff -r 0c8d58332658 -r a9f6994fb906 src/HOL/NatDef.ML
--- 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];