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 no longer works here
authorpaulson
Fri, 12 Dec 1997 10:46:09 +0100
changeset 4393 15544827b0b9
parent 4392 ea41d9c1b0ef
child 4394 c24a1bbd3cf3
new blast_tac no longer works here
src/ZF/Univ.ML file | annotate | diff | comparison | revisions 
--- a/src/ZF/Univ.ML	Fri Dec 12 10:37:45 1997 +0100
+++ b/src/ZF/Univ.ML	Fri Dec 12 10:46:09 1997 +0100
@@ -391,7 +391,8 @@
 
 goal Univ.thy
   "!!a. [| a: Vfrom(A,i);  Limit(i);  Transset(A) |] ==> Pow(a) : Vfrom(A,i)";
-by (blast_tac (claset() addEs [Limit_VfromE]
+(*Blast_tac: PROOF FAILED*)
+by (fast_tac (claset() addEs [Limit_VfromE]
 		       addIs [Limit_has_succ, Pow_in_Vfrom, Limit_VfromI]) 1);
 qed "Pow_in_VLimit";
isabelle