src/HOL/Cardinals/Bounded_Set.thy
changeset 61424 c3658c18b7bc
parent 60247 6a5015b096a2
child 62324 ae44f16dcea5
     1.1 --- a/src/HOL/Cardinals/Bounded_Set.thy	Tue Oct 13 09:21:14 2015 +0200
     1.2 +++ b/src/HOL/Cardinals/Bounded_Set.thy	Tue Oct 13 09:21:15 2015 +0200
     1.3 @@ -50,7 +50,7 @@
     1.4      BNF_Def.Grp {a. set_bset a \<subseteq> {(a, b). R a b}} (map_bset snd)) a b" (is "?L \<longleftrightarrow> ?R")
     1.5  proof
     1.6    assume ?L
     1.7 -  def R' \<equiv> "the_inv set_bset (Collect (split R) \<inter> (set_bset a \<times> set_bset b)) :: ('a \<times> 'b) set['k]"
     1.8 +  def R' \<equiv> "the_inv set_bset (Collect (case_prod R) \<inter> (set_bset a \<times> set_bset b)) :: ('a \<times> 'b) set['k]"
     1.9      (is "the_inv set_bset ?L'")
    1.10    have "|?L'| <o natLeq +c |UNIV :: 'k set|"
    1.11      unfolding csum_def Field_natLeq