Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Hoare/hoareAbort.ML
changeset 17956 369e2af8ee45
parent 15661 9ef583b08647
child 18022 c1bb6480534f 
--- a/src/HOL/Hoare/hoareAbort.ML	Fri Oct 21 18:14:32 2005 +0200
+++ b/src/HOL/Hoare/hoareAbort.ML	Fri Oct 21 18:14:34 2005 +0200
@@ -83,7 +83,7 @@
                            Free ("P",varsT --> boolT) $ Bound 0));
                    val impl = implies $ (Mset_incl big_Collect) $ 
                                           (Mset_incl small_Collect);
-   in Tactic.prove (Thm.sign_of_thm thm) ["Mset", "P"] [] impl (K (CLASET' blast_tac 1)) end;
+   in Goal.prove (Thm.sign_of_thm thm) ["Mset", "P"] [] impl (K (CLASET' blast_tac 1)) end;
 
 end;
isabelle