/src/HOL/TPTP/
drwxr-xr-x [up]
drwxr-xr-x CASC
drwxr-xr-x TPTP_Parser
drwxr-xr-x etc
drwxr-xr-x lib Tools
-rw-r--r-- 2016-03-13 10:22 +0100 572 ATP_Problem_Import.thy
-rw-r--r-- 2016-03-13 10:22 +0100 1305 ATP_Theory_Export.thy
-rw-r--r-- 2016-03-13 10:22 +0100 943 MaSh_Eval.thy
-rw-r--r-- 2016-03-13 10:22 +0100 2359 MaSh_Export.thy
-rw-r--r-- 2016-03-13 10:22 +0100 886 MaSh_Export_Base.thy
-rw-r--r-- 2016-03-13 10:22 +0100 2393 THF_Arith.thy
-rw-r--r-- 2016-03-13 10:22 +0100 423 TPTP_Interpret.thy
-rw-r--r-- 2016-03-13 10:22 +0100 3939 TPTP_Interpret_Test.thy
-rw-r--r-- 2016-03-13 10:22 +0100 1853 TPTP_Parser.thy
-rw-r--r-- 2016-03-13 10:22 +0100 1968 TPTP_Parser_Example.thy
-rw-r--r-- 2016-03-13 10:22 +0100 4062 TPTP_Parser_Test.thy
-rw-r--r-- 2016-03-13 10:22 +0100 75638 TPTP_Proof_Reconstruction.thy
-rw-r--r-- 2016-03-13 10:22 +0100 26503 TPTP_Proof_Reconstruction_Test.thy
-rw-r--r-- 2016-03-13 10:22 +0100 102251 TPTP_Proof_Reconstruction_Test_Units.thy
-rw-r--r-- 2016-03-13 10:22 +0100 2863 TPTP_Test.thy
-rw-r--r-- 2016-03-13 10:22 +0100 12301 atp_problem_import.ML
-rw-r--r-- 2016-03-13 10:22 +0100 14180 atp_theory_export.ML
-rw-r--r-- 2016-03-13 10:22 +0100 6387 mash_eval.ML
-rw-r--r-- 2016-03-13 10:22 +0100 11999 mash_export.ML
-rw-r--r-- 2016-03-13 10:22 +0100 2694 sledgehammer_tactics.ML