src/HOL/Nat.thy

--- a/src/HOL/Nat.thy	Thu Sep 29 00:58:54 2005 +0200
+++ b/src/HOL/Nat.thy	Thu Sep 29 00:58:55 2005 +0200
@@ -24,7 +24,9 @@
   -- {* the axiom of infinity in 2 parts *}
   inj_Suc_Rep:          "inj Suc_Rep"
   Suc_Rep_not_Zero_Rep: "Suc_Rep x \<noteq> Zero_Rep"
-
+finalconsts
+  Zero_Rep
+  Suc_Rep
 
 subsection {* Type nat *}