src/HOL/NatDef.thy

--- a/src/HOL/NatDef.thy	Mon Oct 20 11:22:29 1997 +0200
+++ b/src/HOL/NatDef.thy	Mon Oct 20 11:25:39 1997 +0200
@@ -12,6 +12,8 @@
 
 (** type ind **)
 
+global
+
 types
   ind
 
@@ -59,6 +61,8 @@
   "case p of 0 => a | Suc y => b" == "nat_case a (%y. b) p"
 
 
+local
+
 defs
   Zero_def      "0 == Abs_Nat(Zero_Rep)"
   Suc_def       "Suc == (%n. Abs_Nat(Suc_Rep(Rep_Nat(n))))"