src/HOL/Hoare/Hoare_Logic_Abort.thy
changeset 42174 d0be2722ce9f
parent 42153 fa108629d132
child 44890 22f665a2e91c
     1.1 --- a/src/HOL/Hoare/Hoare_Logic_Abort.thy	Wed Mar 30 22:53:18 2011 +0200
     1.2 +++ b/src/HOL/Hoare/Hoare_Logic_Abort.thy	Wed Mar 30 23:26:40 2011 +0200
     1.3 @@ -10,9 +10,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 @@ -23,7 +22,7 @@
    1.16  
    1.17  abbreviation annskip ("SKIP") where "SKIP == Basic id"
    1.18  
    1.19 -types 'a sem = "'a option => 'a option => bool"
    1.20 +type_synonym 'a sem = "'a option => 'a option => bool"
    1.21  
    1.22  inductive Sem :: "'a com \<Rightarrow> 'a sem"
    1.23  where