Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
New blast_tac call: made possible by bug fix involving equality substitution
authorpaulson
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];
isabelle