src/HOL/TPTP/TPTP_Test.thy
changeset 63167 0909deb8059b
parent 62505 9e2a65912111
     1.1 --- a/src/HOL/TPTP/TPTP_Test.thy	Thu May 26 16:57:14 2016 +0200
     1.2 +++ b/src/HOL/TPTP/TPTP_Test.thy	Thu May 26 17:51:22 2016 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  imports TPTP_Parser
     1.5  begin
     1.6  
     1.7 -ML {*
     1.8 +ML \<open>
     1.9    val tptp_test_out = Attrib.setup_config_string @{binding "tptp_test_out"} (K "")
    1.10    val tptp_test_all = Attrib.setup_config_bool @{binding "tptp_test_all"} (K false)
    1.11    val tptp_test_timeout =
    1.12 @@ -17,27 +17,27 @@
    1.13    fun test_all ctxt = Config.get ctxt tptp_test_all
    1.14    fun get_timeout ctxt = Config.get ctxt tptp_test_timeout
    1.15    fun S x y z = x z (y z)
    1.16 -*}
    1.17 +\<close>
    1.18  
    1.19  section "Parser tests"
    1.20  
    1.21 -ML {*
    1.22 +ML \<open>
    1.23    fun payload_of (TPTP_Syntax.Annotated_Formula (_, _, _, _, fmla, _)) = fmla
    1.24    val payloads_of = map payload_of
    1.25 -*}
    1.26 +\<close>
    1.27  
    1.28  
    1.29  section "Source problems"
    1.30 -ML {*
    1.31 +ML \<open>
    1.32    (*problem source*)
    1.33    val tptp_probs_dir =
    1.34      Path.explode "$TPTP/Problems"
    1.35      |> Path.expand;
    1.36 -*}
    1.37 +\<close>
    1.38  
    1.39  
    1.40  section "Supporting test functions"
    1.41 -ML {*
    1.42 +ML \<open>
    1.43    fun report ctxt str =
    1.44      let
    1.45        val tptp_test_out = Config.get ctxt tptp_test_out
    1.46 @@ -85,10 +85,10 @@
    1.47        report ctxt ("Test timing: " ^ Timing.message time ^ "\n(about " ^ average ^
    1.48         "s per problem)")
    1.49      end
    1.50 -*}
    1.51 +\<close>
    1.52  
    1.53  
    1.54 -ML {*
    1.55 +ML \<open>
    1.56    fun situate file_name = Path.append tptp_probs_dir (Path.explode file_name);
    1.57  
    1.58    fun parser_test ctxt = (*FIXME argument order*)
    1.59 @@ -103,6 +103,6 @@
    1.60  
    1.61    fun parse_timed file =
    1.62      Timing.timing TPTP_Parser.parse_file (Path.implode file)
    1.63 -*}
    1.64 +\<close>
    1.65  
    1.66  end