equal
deleted
inserted
replaced
106 apply (rule decomposition [THEN exE]) |
106 apply (rule decomposition [THEN exE]) |
107 apply (rule exI) |
107 apply (rule exI) |
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, subst 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, subst double_complement, erule inv_image_comp [symmetric]) |
116 done |
116 done |