equal
deleted
inserted
replaced
121 goalw Sum.thy [sum_case_def] "sum_case f g (Inl x) = f(x)"; |
121 goalw Sum.thy [sum_case_def] "sum_case f g (Inl x) = f(x)"; |
122 by (blast_tac (!claset addIs [select_equality]) 1); |
122 by (blast_tac (!claset addIs [select_equality]) 1); |
123 qed "sum_case_Inl"; |
123 qed "sum_case_Inl"; |
124 |
124 |
125 goalw Sum.thy [sum_case_def] "sum_case f g (Inr x) = g(x)"; |
125 goalw Sum.thy [sum_case_def] "sum_case f g (Inr x) = g(x)"; |
126 by (fast_tac (!claset addIs [select_equality]) 1); |
126 by (blast_tac (!claset addIs [select_equality]) 1); |
127 qed "sum_case_Inr"; |
127 qed "sum_case_Inr"; |
128 |
128 |
129 Addsimps [sum_case_Inl, sum_case_Inr]; |
129 Addsimps [sum_case_Inl, sum_case_Inr]; |
130 |
130 |
131 (** Exhaustion rule for sums -- a degenerate form of induction **) |
131 (** Exhaustion rule for sums -- a degenerate form of induction **) |