types -> type_synonym
authorhuffman
Sun Dec 19 18:11:20 2010 -0800 (2010-12-19)
changeset 412955b5388d4ccc9
parent 41294 53df0095b5e4
child 41296 6aaf80ea9715
types -> type_synonym
src/HOL/HOLCF/One.thy
src/HOL/HOLCF/Tr.thy
src/HOL/HOLCF/Universal.thy
     1.1 --- a/src/HOL/HOLCF/One.thy	Sun Dec 19 18:10:54 2010 -0800
     1.2 +++ b/src/HOL/HOLCF/One.thy	Sun Dec 19 18:11:20 2010 -0800
     1.3 @@ -8,14 +8,14 @@
     1.4  imports Lift
     1.5  begin
     1.6  
     1.7 -types one = "unit lift"
     1.8 -translations
     1.9 -  (type) "one" <= (type) "unit lift" 
    1.10 +type_synonym
    1.11 +  one = "unit lift"
    1.12  
    1.13 -definition
    1.14 -  ONE :: "one"
    1.15 -where
    1.16 -  "ONE == Def ()"
    1.17 +translations
    1.18 +  (type) "one" <= (type) "unit lift"
    1.19 +
    1.20 +definition ONE :: "one"
    1.21 +  where "ONE == Def ()"
    1.22  
    1.23  text {* Exhaustion and Elimination for type @{typ one} *}
    1.24  
     2.1 --- a/src/HOL/HOLCF/Tr.thy	Sun Dec 19 18:10:54 2010 -0800
     2.2 +++ b/src/HOL/HOLCF/Tr.thy	Sun Dec 19 18:11:20 2010 -0800
     2.3 @@ -10,7 +10,7 @@
     2.4  
     2.5  subsection {* Type definition and constructors *}
     2.6  
     2.7 -types
     2.8 +type_synonym
     2.9    tr = "bool lift"
    2.10  
    2.11  translations
     3.1 --- a/src/HOL/HOLCF/Universal.thy	Sun Dec 19 18:10:54 2010 -0800
     3.2 +++ b/src/HOL/HOLCF/Universal.thy	Sun Dec 19 18:11:20 2010 -0800
     3.3 @@ -12,7 +12,7 @@
     3.4  
     3.5  subsubsection {* Basis datatype *}
     3.6  
     3.7 -types ubasis = nat
     3.8 +type_synonym ubasis = nat
     3.9  
    3.10  definition
    3.11    node :: "nat \<Rightarrow> ubasis \<Rightarrow> ubasis set \<Rightarrow> ubasis"