src/HOL/Nat.thy
changeset 49834 b27bbb021df1
parent 49723 bbc2942ba09f
child 49962 a8cc904a6820
     1.1 --- a/src/HOL/Nat.thy	Fri Oct 12 15:08:29 2012 +0200
     1.2 +++ b/src/HOL/Nat.thy	Fri Oct 12 18:58:20 2012 +0200
     1.3 @@ -33,7 +33,7 @@
     1.4    Zero_RepI: "Nat Zero_Rep"
     1.5  | Suc_RepI: "Nat i \<Longrightarrow> Nat (Suc_Rep i)"
     1.6  
     1.7 -typedef (open) nat = "{n. Nat n}"
     1.8 +typedef nat = "{n. Nat n}"
     1.9    morphisms Rep_Nat Abs_Nat
    1.10    using Nat.Zero_RepI by auto
    1.11