/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-- 2020-07-06 16:52 +0200 707 ATP_Problem_Import.thy
-rw-r--r-- 2020-07-06 16:52 +0200 1420 ATP_Theory_Export.thy
-rw-r--r-- 2020-07-06 16:52 +0200 1016 MaSh_Eval.thy
-rw-r--r-- 2020-07-06 16:52 +0200 2533 MaSh_Export.thy
-rw-r--r-- 2020-07-06 16:52 +0200 951 MaSh_Export_Base.thy
-rw-r--r-- 2020-07-06 16:52 +0200 2393 THF_Arith.thy
-rw-r--r-- 2020-07-06 16:52 +0200 436 TPTP_Interpret.thy
-rw-r--r-- 2020-07-06 16:52 +0200 4027 TPTP_Interpret_Test.thy
-rw-r--r-- 2020-07-06 16:52 +0200 1953 TPTP_Parser.thy
-rw-r--r-- 2020-07-06 16:52 +0200 2034 TPTP_Parser_Example.thy
-rw-r--r-- 2020-07-06 16:52 +0200 4166 TPTP_Parser_Test.thy
-rw-r--r-- 2020-07-06 16:52 +0200 77639 TPTP_Proof_Reconstruction.thy
-rw-r--r-- 2020-07-06 16:52 +0200 26692 TPTP_Proof_Reconstruction_Test.thy
-rw-r--r-- 2020-07-06 16:52 +0200 103165 TPTP_Proof_Reconstruction_Test_Units.thy
-rw-r--r-- 2020-07-06 16:52 +0200 2918 TPTP_Test.thy
-rw-r--r-- 2020-07-06 16:52 +0200 12056 atp_problem_import.ML
-rw-r--r-- 2020-07-06 16:52 +0200 14246 atp_theory_export.ML
-rw-r--r-- 2020-07-06 16:52 +0200 6373 mash_eval.ML
-rw-r--r-- 2020-07-06 16:52 +0200 11989 mash_export.ML
-rw-r--r-- 2020-07-06 16:52 +0200 2711 sledgehammer_tactics.ML