src/HOL/TPTP/ATP_Theory_Export.thy
changeset 48375 48628962976b
parent 48302 6cf5e58f1185
child 48891 c0eafbd55de3
equal deleted inserted replaced
48374:623607c5a40f 48375:48628962976b
     8 imports Complex_Main
     8 imports Complex_Main
     9 uses "atp_theory_export.ML"
     9 uses "atp_theory_export.ML"
    10 begin
    10 begin
    11 
    11 
    12 ML {*
    12 ML {*
    13 open ATP_Problem;
    13 open ATP_Problem
    14 open ATP_Theory_Export;
    14 open ATP_Theory_Export
    15 *}
    15 *}
    16 
    16 
    17 ML {*
    17 ML {*
    18 val do_it = false; (* switch to "true" to generate the files *)
    18 val do_it = false (* switch to "true" to generate the files *)
    19 val thy = @{theory List};
    19 val thy = @{theory List}
    20 val ctxt = @{context}
    20 val ctxt = @{context}
    21 *}
    21 *}
    22 
    22 
    23 ML {*
    23 ML {*
    24 if do_it then
    24 if do_it then