# 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 {*