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.
to handle non-atomic assumptions
authorpaulson
Tue, 03 Jul 2007 21:56:25 +0200
changeset 23552 6403d06abe25
parent 23551 84f0996a530b
child 23553 af8ae54238f5
to handle non-atomic assumptions
src/HOL/Tools/meson.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/meson.ML	Tue Jul 03 20:26:08 2007 +0200
+++ b/src/HOL/Tools/meson.ML	Tue Jul 03 21:56:25 2007 +0200
@@ -556,7 +556,8 @@
   Function mkcl converts theorems to clauses.*)
 fun MESON mkcl cltac i st = 
   SELECT_GOAL
-    (EVERY [rtac ccontr 1,
+    (EVERY [ObjectLogic.atomize_tac 1,
+            rtac ccontr 1,
 	    METAHYPS (fn negs =>
 		      EVERY1 [skolemize_prems_tac negs,
 			      METAHYPS (cltac o mkcl)]) 1]) i st
isabelle