# HG changeset patch
# User sultana
# Date 1335180203 -3600
# Node ID 64023cf4d1488accdb04d15acb677ee6ce45d7a9
# Parent  3d76c81b5ed2c8b465ecf8fbaa8760f3fc5d0d28
updated test;

diff -r 3d76c81b5ed2 -r 64023cf4d148 src/HOL/TPTP/TPTP_Interpret_Test.thy
--- a/src/HOL/TPTP/TPTP_Interpret_Test.thy	Mon Apr 23 12:23:23 2012 +0100
+++ b/src/HOL/TPTP/TPTP_Interpret_Test.thy	Mon Apr 23 12:23:23 2012 +0100
@@ -18,12 +18,13 @@
       (TPTP_Interpret.interpret_file
        false
        (Path.dir tptp_probs_dir)
-      (Path.append tptp_probs_dir (Path.explode "LCL/LCL825-1.p"))
+       (Path.append tptp_probs_dir (Path.explode "LCL/LCL825-1.p"))
        []
        [])
       @{theory}
 *}
 
+
 text "... and display nicely."
 ML {*
   List.app (Pretty.writeln o (Syntax.pretty_term @{context}) o #3) fmlas;
@@ -100,13 +101,16 @@
      "GEG/GEG018^1.p",
      "SYN/SYN045^4.p",
      "SYN/SYN001^4.001.p",
-     "SYN/SYN000^2.p",
      "SYN/SYN387^4.p",
      "SYN/SYN393^4.002.p",
      "SYN/SYN978^4.p",
      "SYN/SYN044^4.p",
      "SYN/SYN393^4.003.p",
-     "SYN/SYN389^4.p"]
+     "SYN/SYN389^4.p",
+     "ARI/ARI625=1.p",
+     "SYO/SYO561_2.p",
+     "SYO/SYO562_1.p",
+     "SYN/SYN000_2.p"]
 *}
 
 ML {*