src/HOL/ex/CTL.thy
changeset 42463 f270e3e18be5
parent 41460 ea56b98aee83
child 46008 c296c75f4cf4
     1.1 --- a/src/HOL/ex/CTL.thy	Fri Apr 22 15:57:43 2011 +0200
     1.2 +++ b/src/HOL/ex/CTL.thy	Sat Apr 23 13:00:19 2011 +0200
     1.3 @@ -21,7 +21,7 @@
     1.4  
     1.5  lemmas [intro!] = Int_greatest Un_upper2 Un_upper1 Int_lower1 Int_lower2
     1.6  
     1.7 -types 'a ctl = "'a set"
     1.8 +type_synonym 'a ctl = "'a set"
     1.9  
    1.10  definition
    1.11    imp :: "'a ctl \<Rightarrow> 'a ctl \<Rightarrow> 'a ctl"    (infixr "\<rightarrow>" 75) where