src/HOL/Bali/Basis.thy
changeset 61424 c3658c18b7bc
parent 59755 f8d164ab0dc1
child 62042 6c6ccf573479
     1.1 --- a/src/HOL/Bali/Basis.thy	Tue Oct 13 09:21:14 2015 +0200
     1.2 +++ b/src/HOL/Bali/Basis.thy	Tue Oct 13 09:21:15 2015 +0200
     1.3 @@ -16,7 +16,7 @@
     1.4  declare if_weak_cong [cong del] option.case_cong_weak [cong del]
     1.5  declare length_Suc_conv [iff]
     1.6  
     1.7 -lemma Collect_split_eq: "{p. P (split f p)} = {(a,b). P (f a b)}"
     1.8 +lemma Collect_split_eq: "{p. P (case_prod f p)} = {(a,b). P (f a b)}"
     1.9    by auto
    1.10  
    1.11  lemma subset_insertD: "A \<subseteq> insert x B \<Longrightarrow> A \<subseteq> B \<and> x \<notin> A \<or> (\<exists>B'. A = insert x B' \<and> B' \<subseteq> B)"