src/HOL/UNITY/Transformers.thy
changeset 30952 7ab2716dd93b
parent 26806 40b411ec05aa
child 30971 7fbebf75b3ef
     1.1 --- a/src/HOL/UNITY/Transformers.thy	Fri Apr 17 16:41:31 2009 +0200
     1.2 +++ b/src/HOL/UNITY/Transformers.thy	Mon Apr 20 09:32:07 2009 +0200
     1.3 @@ -338,10 +338,10 @@
     1.4  
     1.5  constdefs
     1.6    wens_single_finite :: "[('a*'a) set, 'a set, nat] => 'a set"  
     1.7 -    "wens_single_finite act B k == \<Union>i \<in> atMost k. ((wp act)^i) B"
     1.8 +    "wens_single_finite act B k == \<Union>i \<in> atMost k. (wp act o^ i) B"
     1.9  
    1.10    wens_single :: "[('a*'a) set, 'a set] => 'a set"  
    1.11 -    "wens_single act B == \<Union>i. ((wp act)^i) B"
    1.12 +    "wens_single act B == \<Union>i. (wp act o^ i) B"
    1.13  
    1.14  lemma wens_single_Un_eq:
    1.15        "single_valued act