src/HOL/Lifting_Set.thy
changeset 60057 86fa63ce8156
parent 58889 5b7a9633cfa8
child 60229 4cd6462c1fda
     1.1 --- a/src/HOL/Lifting_Set.thy	Mon Apr 13 13:03:41 2015 +0200
     1.2 +++ b/src/HOL/Lifting_Set.thy	Tue Apr 14 11:32:01 2015 +0200
     1.3 @@ -281,4 +281,9 @@
     1.4  lemmas setsum_parametric = setsum.F_parametric
     1.5  lemmas setprod_parametric = setprod.F_parametric
     1.6  
     1.7 +lemma rel_set_UNION:
     1.8 +  assumes [transfer_rule]: "rel_set Q A B" "rel_fun Q (rel_set R) f g"
     1.9 +  shows "rel_set R (UNION A f) (UNION B g)"
    1.10 +by transfer_prover
    1.11 +
    1.12  end