simplify a proof due to 6c95a39348bd
authorkuncar
Tue Feb 25 19:07:42 2014 +0100 (2014-02-25)
changeset 55738303123344459
parent 55737 84f6ac9f6e41
child 55753 c90cc76ec855
simplify a proof due to 6c95a39348bd
src/HOL/Library/FSet.thy
     1.1 --- a/src/HOL/Library/FSet.thy	Tue Feb 25 19:07:40 2014 +0100
     1.2 +++ b/src/HOL/Library/FSet.thy	Tue Feb 25 19:07:42 2014 +0100
     1.3 @@ -186,9 +186,8 @@
     1.4  
     1.5  lift_definition fthe_elem :: "'a fset \<Rightarrow> 'a" is the_elem .
     1.6  
     1.7 -(* FIXME why is not invariant here unfolded ? *)
     1.8 -lift_definition fbind :: "'a fset \<Rightarrow> ('a \<Rightarrow> 'b fset) \<Rightarrow> 'b fset" is Set.bind parametric bind_transfer
     1.9 -unfolding invariant_def Set.bind_def by clarsimp metis
    1.10 +lift_definition fbind :: "'a fset \<Rightarrow> ('a \<Rightarrow> 'b fset) \<Rightarrow> 'b fset" is Set.bind parametric bind_transfer 
    1.11 +by (simp add: Set.bind_def)
    1.12  
    1.13  lift_definition ffUnion :: "'a fset fset \<Rightarrow> 'a fset" is Union parametric Union_transfer by simp
    1.14