| changeset 60585 | 48fdff264eb2 |
| parent 44890 | 22f665a2e91c |
| child 62042 | 6c6ccf573479 |
--- a/src/HOL/Hoare/SchorrWaite.thy Fri Jun 26 00:14:10 2015 +0200 +++ b/src/HOL/Hoare/SchorrWaite.thy Fri Jun 26 10:20:33 2015 +0200 @@ -17,7 +17,7 @@ definition relS :: "('a \<Rightarrow> 'a ref) set \<Rightarrow> ('a \<times> 'a) set" - where "relS M = (\<Union> m \<in> M. rel m)" + where "relS M = (\<Union>m \<in> M. rel m)" definition addrs :: "'a ref set \<Rightarrow> 'a set"