src/HOL/Library/FuncSet.thy
changeset 62390 842917225d56
parent 61955 e96292f32c3c
child 63060 293ede07b775
     1.1 --- a/src/HOL/Library/FuncSet.thy	Tue Feb 23 15:37:18 2016 +0100
     1.2 +++ b/src/HOL/Library/FuncSet.thy	Tue Feb 23 16:25:08 2016 +0100
     1.3 @@ -151,7 +151,7 @@
     1.4  lemma Pi_fupd_iff: "i \<in> I \<Longrightarrow> f \<in> Pi I (B(i := A)) \<longleftrightarrow> f \<in> Pi (I - {i}) B \<and> f i \<in> A"
     1.5    apply auto
     1.6    apply (drule_tac x=x in Pi_mem)
     1.7 -  apply (simp_all split: split_if_asm)
     1.8 +  apply (simp_all split: if_split_asm)
     1.9    apply (drule_tac x=i in Pi_mem)
    1.10    apply (auto dest!: Pi_mem)
    1.11    done
    1.12 @@ -527,7 +527,7 @@
    1.13    apply (auto intro: PiE_mem del: PiE_I PiE_E)
    1.14    apply (rule_tac x="xa(x := undefined)" in exI)
    1.15    apply (auto intro!: extensional_funcset_fun_upd_restricts_rangeI)
    1.16 -  apply (auto dest!: PiE_mem split: split_if_asm)
    1.17 +  apply (auto dest!: PiE_mem split: if_split_asm)
    1.18    done
    1.19  
    1.20  lemma extensional_funcset_extend_domain_inj_onI:
    1.21 @@ -555,7 +555,7 @@
    1.22      unfolding fun_eq_iff by auto
    1.23    from this[of x] show "y = z" by simp
    1.24    fix i from *[of i] \<open>x \<notin> S\<close> fg show "f i = g i"
    1.25 -    by (auto split: split_if_asm simp: PiE_def extensional_def)
    1.26 +    by (auto split: if_split_asm simp: PiE_def extensional_def)
    1.27  qed
    1.28  
    1.29  lemma card_PiE: "finite S \<Longrightarrow> card (\<Pi>\<^sub>E i \<in> S. T i) = (\<Prod> i\<in>S. card (T i))"