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.
a faster proof
authorpaulson
Mon, 16 Nov 1998 13:58:48 +0100
changeset 5898 3e34e7aa7479
parent 5897 b3548f939dd2
child 5899 13d4753079fe
a faster proof
src/HOL/UNITY/Union.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/UNITY/Union.ML	Mon Nov 16 13:54:35 1998 +0100
+++ b/src/HOL/UNITY/Union.ML	Mon Nov 16 13:58:48 1998 +0100
@@ -237,7 +237,7 @@
 Goalw [localTo_def, stable_def, constrains_def]
      "v localTo F <= (f o v) localTo F";
 by (Clarify_tac 1);
-by (auto_tac (claset() addSEs [allE, ballE], simpset()));
+by (force_tac (claset() addSEs [allE, ballE], simpset()) 1);
 qed "localTo_imp_o_localTo";
isabelle