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.
use raw monomorphic encoding with Waldmeister, to avoid overloading it with too many function symbols (as would be the case using mangled monomorphic encodings)
authorblanchet
Thu, 10 May 2012 10:07:40 +0200
changeset 47898 6213900d6d5f
parent 47897 9d978604aee4
child 47899 493d70c63fd6
use raw monomorphic encoding with Waldmeister, to avoid overloading it with too many function symbols (as would be the case using mangled monomorphic encodings)
src/HOL/Tools/ATP/atp_systems.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/ATP/atp_systems.ML	Wed May 09 11:24:38 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Thu May 10 10:07:40 2012 +0200
@@ -641,7 +641,7 @@
        (Inappropriate, "****  Unexpected end of file."),
        (Crashed, "Unrecoverable Segmentation Fault")]
       Hypothesis Hypothesis
-      (K ((50, CNF_UEQ, "mono_tags??", combsN, false), "") (* FUDGE *))
+      (K ((50, CNF_UEQ, "raw_mono_tags??", combsN, false), "") (* FUDGE *))
 
 (* Setup *)
isabelle