src/HOL/Hoare/Hoare_Logic.thy
changeset 42174 d0be2722ce9f
parent 42153 fa108629d132
child 48891 c0eafbd55de3
     1.1 --- a/src/HOL/Hoare/Hoare_Logic.thy	Wed Mar 30 22:53:18 2011 +0200
     1.2 +++ b/src/HOL/Hoare/Hoare_Logic.thy	Wed Mar 30 23:26:40 2011 +0200
     1.3 @@ -13,9 +13,8 @@
     1.4  uses ("hoare_syntax.ML") ("hoare_tac.ML")
     1.5  begin
     1.6  
     1.7 -types
     1.8 -    'a bexp = "'a set"
     1.9 -    'a assn = "'a set"
    1.10 +type_synonym 'a bexp = "'a set"
    1.11 +type_synonym 'a assn = "'a set"
    1.12  
    1.13  datatype
    1.14   'a com = Basic "'a \<Rightarrow> 'a"
    1.15 @@ -25,7 +24,7 @@
    1.16  
    1.17  abbreviation annskip ("SKIP") where "SKIP == Basic id"
    1.18  
    1.19 -types 'a sem = "'a => 'a => bool"
    1.20 +type_synonym 'a sem = "'a => 'a => bool"
    1.21  
    1.22  inductive Sem :: "'a com \<Rightarrow> 'a sem"
    1.23  where