# HG changeset patch
# User blanchet
# Date 1342815585 -7200
# Node ID 48628962976b56f62e2762572c58ea4fc012c5d6
# Parent  623607c5a40f1cf69dff83e05ce6fbdaa802a063
tuning

diff -r 623607c5a40f -r 48628962976b src/HOL/TPTP/ATP_Theory_Export.thy
--- a/src/HOL/TPTP/ATP_Theory_Export.thy	Fri Jul 20 21:05:47 2012 +0200
+++ b/src/HOL/TPTP/ATP_Theory_Export.thy	Fri Jul 20 22:19:45 2012 +0200
@@ -10,13 +10,13 @@
 begin
 
 ML {*
-open ATP_Problem;
-open ATP_Theory_Export;
+open ATP_Problem
+open ATP_Theory_Export
 *}
 
 ML {*
-val do_it = false; (* switch to "true" to generate the files *)
-val thy = @{theory List};
+val do_it = false (* switch to "true" to generate the files *)
+val thy = @{theory List}
 val ctxt = @{context}
 *}