# HG changeset patch
# User webertj
# Date 1156774244 -7200
# Node ID 56ef2dfc41d63cefbc6f056e7c9dbe6cdd19641e
# Parent  df257a9cf0e9d25c94961ebd22f3f0e52a595b50
encode clauses as Isar premises, rather than as object-logic &, for faster parsing

diff -r df257a9cf0e9 -r 56ef2dfc41d6 lib/scripts/dimacs2hol.pl
--- a/lib/scripts/dimacs2hol.pl	Fri Aug 25 18:48:58 2006 +0200
+++ b/lib/scripts/dimacs2hol.pl	Mon Aug 28 16:10:44 2006 +0200
@@ -42,7 +42,7 @@
     s/(\s+0)?\s*\z//;                        # remove trailing whitespace, and possibly a last '0'
     s/-/~/g;                                 # replace '-' by '~' (negation in HOL)
     s/[1-9]\d*/v$&/g;                        # add 'v' before variables
-    s/(\s+)0(\s+)/\)$1&$2\(/g;               # replace ' 0 ' by ') & ('
+    s/\s+0\s+/\"\nand \"/g;                  # replace ' 0 ' by '"\nand "'
     s/(\d)(\s+[~v])/$1 |$2/g;                # insert ' |' between literals
 
     my ($filename) = $file;
@@ -62,9 +62,10 @@
     print FILE "\\end{verbatim}\n";
     print FILE "*}\n";
     print FILE "\n";
-    print FILE "theorem \"~((";  # negate the whole CNF formula
-    print FILE;
-    print FILE "))\"\n";
+    print FILE "theorem assumes \""; print FILE;
+    print FILE "\"\n";
+    print FILE "shows \"False\"\n";  # negate the whole CNF formula
+    print FILE "using prems\n";
     print FILE "oops\n";
     print FILE "\n";
     print FILE "end\n";