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.
do not declare TPTP built-ins, e.g. $true
authorblanchet
Mon, 02 May 2011 23:01:22 +0200
changeset 42645 242bc53b98e5
parent 42644 9dd98edd48c2
child 42646 4781fcd53572
do not declare TPTP built-ins, e.g. $true
src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Mon May 02 22:52:15 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Mon May 02 23:01:22 2011 +0200
@@ -811,6 +811,7 @@
 
 fun should_declare_sym type_sys pred_sym s =
   not (String.isPrefix bound_var_prefix s) andalso s <> "equal" andalso
+  not (String.isPrefix "$" s) andalso
   (type_sys = Many_Typed orelse not pred_sym)
 
 fun add_combterm_syms_to_decl_table type_sys repaired_sym_tab =
isabelle