src/HOL/NSA/HyperNat.thy
changeset 42463 f270e3e18be5
parent 37765 26bdfb7b680b
child 57512 cc97b347b301
--- a/src/HOL/NSA/HyperNat.thy	Fri Apr 22 15:57:43 2011 +0200
+++ b/src/HOL/NSA/HyperNat.thy	Sat Apr 23 13:00:19 2011 +0200
@@ -11,7 +11,7 @@
 imports StarDef
 begin
 
-types hypnat = "nat star"
+type_synonym hypnat = "nat star"
 
 abbreviation
   hypnat_of_nat :: "nat => nat star" where