author | blanchet |
Fri, 20 Jul 2012 22:19:45 +0200 | |
changeset 48375 | 48628962976b |
parent 48374 | 623607c5a40f |
child 48376 | 416e4123baf3 |
--- 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} *}