summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/Sum.ML

changeset 3091 | 9366415b93ad |

parent 2922 | 580647a879cf |

child 3842 | b55686a7b22c |

equal
deleted
inserted
replaced

3090:eeb4d0c7f748 | 3091:9366415b93ad |
---|---|

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 **) |