src/HOL/ex/set.thy
changeset 15481 fc075ae929e4
parent 15306 51f3d31e8eea
child 15488 7c638a46dcbb
equal deleted inserted replaced
15480:cb3612cc41a3 15481:fc075ae929e4
   108   apply (rule bij_if_then_else)
   108   apply (rule bij_if_then_else)
   109      apply (rule_tac [4] refl)
   109      apply (rule_tac [4] refl)
   110     apply (rule_tac [2] inj_on_inv)
   110     apply (rule_tac [2] inj_on_inv)
   111     apply (erule subset_inj_on [OF _ subset_UNIV])
   111     apply (erule subset_inj_on [OF _ subset_UNIV])
   112    txt {* Tricky variable instantiations! *}
   112    txt {* Tricky variable instantiations! *}
   113    apply (erule ssubst, subst double_complement)
   113    apply (erule ssubst, simplesubst double_complement)
   114    apply (rule subsetI, erule imageE, erule ssubst, rule rangeI)
   114    apply (rule subsetI, erule imageE, erule ssubst, rule rangeI)
   115   apply (erule ssubst, subst double_complement, erule inv_image_comp [symmetric])
   115   apply (erule ssubst, simplesubst double_complement, erule inv_image_comp [symmetric])
   116   done
   116   done
   117 
   117 
   118 
   118 
   119 subsection {* Set variable instantiation examples *}
   119 subsection {* Set variable instantiation examples *}
   120 
   120