summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | paulson |

Fri, 02 May 1997 10:17:44 +0200 | |

changeset 3091 | 9366415b93ad |

parent 3090 | eeb4d0c7f748 |

child 3092 | b92a1b50b16b |

New blast_tac call: made possible by bug fix involving equality substitution

src/HOL/Sum.ML | file | annotate | diff | comparison | revisions |

--- a/src/HOL/Sum.ML Thu May 01 10:28:10 1997 +0200 +++ b/src/HOL/Sum.ML Fri May 02 10:17:44 1997 +0200 @@ -123,7 +123,7 @@ qed "sum_case_Inl"; goalw Sum.thy [sum_case_def] "sum_case f g (Inr x) = g(x)"; -by (fast_tac (!claset addIs [select_equality]) 1); +by (blast_tac (!claset addIs [select_equality]) 1); qed "sum_case_Inr"; Addsimps [sum_case_Inl, sum_case_Inr];