# HG changeset patch
# User huffman
# Date 1292811080 28800
# Node ID 5b5388d4ccc930cf38297788eb407be3b8bc525b
# Parent  53df0095b5e4e464d3c036d0a70a7b22daa3db4f
types -> type_synonym

diff -r 53df0095b5e4 -r 5b5388d4ccc9 src/HOL/HOLCF/One.thy
--- a/src/HOL/HOLCF/One.thy	Sun Dec 19 18:10:54 2010 -0800
+++ b/src/HOL/HOLCF/One.thy	Sun Dec 19 18:11:20 2010 -0800
@@ -8,14 +8,14 @@
 imports Lift
 begin
 
-types one = "unit lift"
-translations
-  (type) "one" <= (type) "unit lift" 
+type_synonym
+  one = "unit lift"
 
-definition
-  ONE :: "one"
-where
-  "ONE == Def ()"
+translations
+  (type) "one" <= (type) "unit lift"
+
+definition ONE :: "one"
+  where "ONE == Def ()"
 
 text {* Exhaustion and Elimination for type @{typ one} *}
 
diff -r 53df0095b5e4 -r 5b5388d4ccc9 src/HOL/HOLCF/Tr.thy
--- a/src/HOL/HOLCF/Tr.thy	Sun Dec 19 18:10:54 2010 -0800
+++ b/src/HOL/HOLCF/Tr.thy	Sun Dec 19 18:11:20 2010 -0800
@@ -10,7 +10,7 @@
 
 subsection {* Type definition and constructors *}
 
-types
+type_synonym
   tr = "bool lift"
 
 translations
diff -r 53df0095b5e4 -r 5b5388d4ccc9 src/HOL/HOLCF/Universal.thy
--- a/src/HOL/HOLCF/Universal.thy	Sun Dec 19 18:10:54 2010 -0800
+++ b/src/HOL/HOLCF/Universal.thy	Sun Dec 19 18:11:20 2010 -0800
@@ -12,7 +12,7 @@
 
 subsubsection {* Basis datatype *}
 
-types ubasis = nat
+type_synonym ubasis = nat
 
 definition
   node :: "nat \<Rightarrow> ubasis \<Rightarrow> ubasis set \<Rightarrow> ubasis"