src/HOL/Hoare_Parallel/RG_Hoare.thy
changeset 42174 d0be2722ce9f
parent 41842 d8f76db6a207
child 52597 a8a81453833d
     1.1 --- a/src/HOL/Hoare_Parallel/RG_Hoare.thy	Wed Mar 30 22:53:18 2011 +0200
     1.2 +++ b/src/HOL/Hoare_Parallel/RG_Hoare.thy	Wed Mar 30 23:26:40 2011 +0200
     1.3 @@ -55,7 +55,8 @@
     1.4  
     1.5  subsection {* Proof System for Parallel Programs *}
     1.6  
     1.7 -types 'a par_rgformula = "('a rgformula) list \<times> 'a set \<times> ('a \<times> 'a) set \<times> ('a \<times> 'a) set \<times> 'a set"
     1.8 +type_synonym 'a par_rgformula =
     1.9 +  "('a rgformula) list \<times> 'a set \<times> ('a \<times> 'a) set \<times> ('a \<times> 'a) set \<times> 'a set"
    1.10  
    1.11  inductive
    1.12    par_rghoare :: "('a rgformula) list \<Rightarrow> 'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> 'a set \<Rightarrow> bool"