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/Tools/Sledgehammer/sledgehammer_tptp_format.ML
changeset 38005 b6555e9c5de4
parent 38004 43fdc7c259ea
child 38006 31001bc88c1a 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML	Mon Jul 26 22:35:25 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML	Mon Jul 26 23:54:40 2010 +0200
@@ -77,6 +77,8 @@
 fun string_for_formula (AQuant (q, xs, phi)) =
     string_for_quantifier q ^ "[" ^ commas xs ^ "]: " ^
     string_for_formula phi
+  | string_for_formula (AConn (ANot, [APred (ATerm ("equal", ts))])) =
+    space_implode " != " (map string_for_term ts)
   | string_for_formula (AConn (c, [phi])) =
     string_for_connective c ^ " " ^ string_for_formula phi
   | string_for_formula (AConn (c, phis)) =
isabelle