--- a/src/HOL/UNITY/Transformers.thy Fri Apr 17 16:41:31 2009 +0200
+++ b/src/HOL/UNITY/Transformers.thy Mon Apr 20 09:32:07 2009 +0200
@@ -338,10 +338,10 @@
constdefs
wens_single_finite :: "[('a*'a) set, 'a set, nat] => 'a set"
- "wens_single_finite act B k == \<Union>i \<in> atMost k. ((wp act)^i) B"
+ "wens_single_finite act B k == \<Union>i \<in> atMost k. (wp act o^ i) B"
wens_single :: "[('a*'a) set, 'a set] => 'a set"
- "wens_single act B == \<Union>i. ((wp act)^i) B"
+ "wens_single act B == \<Union>i. (wp act o^ i) B"
lemma wens_single_Un_eq:
"single_valued act