/src/HOL/TPTP/
drwxr-xr-x [up]
drwxr-xr-x TPTP_Parser
drwxr-xr-x etc
drwxr-xr-x lib Tools
-rw-r--r-- 2012-07-24 21:36 +0200 576 ATP_Problem_Import.thy
-rw-r--r-- 2012-07-24 21:36 +0200 874 ATP_Theory_Export.thy
-rw-r--r-- 2012-07-24 21:36 +0200 705 MaSh_Eval.thy
-rw-r--r-- 2012-07-24 21:36 +0200 1222 MaSh_Export.thy
-rw-r--r-- 2012-07-24 21:36 +0200 378 ROOT.ML
-rw-r--r-- 2012-07-24 21:36 +0200 2483 THF_Arith.thy
-rw-r--r-- 2012-07-24 21:36 +0200 451 TPTP_Interpret.thy
-rw-r--r-- 2012-07-24 21:36 +0200 3912 TPTP_Interpret_Test.thy
-rw-r--r-- 2012-07-24 21:36 +0200 1821 TPTP_Parser.thy
-rw-r--r-- 2012-07-24 21:36 +0200 1905 TPTP_Parser_Example.thy
-rw-r--r-- 2012-07-24 21:36 +0200 3994 TPTP_Parser_Test.thy
-rw-r--r-- 2012-07-24 21:36 +0200 2960 TPTP_Test.thy
-rw-r--r-- 2012-07-24 21:36 +0200 11011 atp_problem_import.ML
-rw-r--r-- 2012-07-24 21:36 +0200 6636 atp_theory_export.ML
-rw-r--r-- 2012-07-24 21:36 +0200 5002 mash_eval.ML
-rw-r--r-- 2012-07-24 21:36 +0200 6826 mash_export.ML
-rw-r--r-- 2012-07-24 21:36 +0200 3032 sledgehammer_tactics.ML