src/HOL/TPTP/TPTP_Interpret_Test.thy
changeset 47693 64023cf4d148
parent 47558 55b42f9af99d
child 48829 6ed588c4f963
     1.1 --- a/src/HOL/TPTP/TPTP_Interpret_Test.thy	Mon Apr 23 12:23:23 2012 +0100
     1.2 +++ b/src/HOL/TPTP/TPTP_Interpret_Test.thy	Mon Apr 23 12:23:23 2012 +0100
     1.3 @@ -18,12 +18,13 @@
     1.4        (TPTP_Interpret.interpret_file
     1.5         false
     1.6         (Path.dir tptp_probs_dir)
     1.7 -      (Path.append tptp_probs_dir (Path.explode "LCL/LCL825-1.p"))
     1.8 +       (Path.append tptp_probs_dir (Path.explode "LCL/LCL825-1.p"))
     1.9         []
    1.10         [])
    1.11        @{theory}
    1.12  *}
    1.13  
    1.14 +
    1.15  text "... and display nicely."
    1.16  ML {*
    1.17    List.app (Pretty.writeln o (Syntax.pretty_term @{context}) o #3) fmlas;
    1.18 @@ -100,13 +101,16 @@
    1.19       "GEG/GEG018^1.p",
    1.20       "SYN/SYN045^4.p",
    1.21       "SYN/SYN001^4.001.p",
    1.22 -     "SYN/SYN000^2.p",
    1.23       "SYN/SYN387^4.p",
    1.24       "SYN/SYN393^4.002.p",
    1.25       "SYN/SYN978^4.p",
    1.26       "SYN/SYN044^4.p",
    1.27       "SYN/SYN393^4.003.p",
    1.28 -     "SYN/SYN389^4.p"]
    1.29 +     "SYN/SYN389^4.p",
    1.30 +     "ARI/ARI625=1.p",
    1.31 +     "SYO/SYO561_2.p",
    1.32 +     "SYO/SYO562_1.p",
    1.33 +     "SYN/SYN000_2.p"]
    1.34  *}
    1.35  
    1.36  ML {*