generalised type
authornipkow
Wed Jan 04 13:58:06 2012 +0100 (2012-01-04)
changeset 46116b903d272c37d
parent 46115 ecab67f5a5c2
child 46117 edd50ec8d471
generalised type
src/HOL/IMP/Collecting.thy
     1.1 --- a/src/HOL/IMP/Collecting.thy	Wed Jan 04 12:09:53 2012 +0100
     1.2 +++ b/src/HOL/IMP/Collecting.thy	Wed Jan 04 13:58:06 2012 +0100
     1.3 @@ -75,7 +75,7 @@
     1.4  fun invar :: "'a acom \<Rightarrow> 'a" where
     1.5  "invar({I} WHILE b DO c {P}) = I"
     1.6  
     1.7 -fun lift :: "('a set \<Rightarrow> 'a) \<Rightarrow> com \<Rightarrow> 'a acom set \<Rightarrow> 'a acom"
     1.8 +fun lift :: "('a set \<Rightarrow> 'b) \<Rightarrow> com \<Rightarrow> 'a acom set \<Rightarrow> 'b acom"
     1.9  where
    1.10  "lift F com.SKIP M = (SKIP {F (post ` M)})" |
    1.11  "lift F (x ::= a) M = (x ::= a {F (post ` M)})" |