src/HOL/UNITY/Transformers.thy
changeset 30971 7fbebf75b3ef
parent 30952 7ab2716dd93b
child 32587 caa5ada96a00
     1.1 --- a/src/HOL/UNITY/Transformers.thy	Fri Apr 24 08:24:54 2009 +0200
     1.2 +++ b/src/HOL/UNITY/Transformers.thy	Fri Apr 24 17:45:15 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 o^ i) B"
     1.8 +    "wens_single_finite act B k == \<Union>i \<in> atMost k. (wp act ^^ 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 o^ i) B"
    1.12 +    "wens_single act B == \<Union>i. (wp act ^^ i) B"
    1.13  
    1.14  lemma wens_single_Un_eq:
    1.15        "single_valued act