Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/TPTP/ATP_Problem_Import.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 46324 e4bccf5ec61e
child 47557 32f35b3d9e42
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
46324
e4bccf5ec61e added problem importer
blanchet
parents:
diff changeset 
     1
 
(*  Title:      HOL/TPTP/ATP_Problem_Import.thy
e4bccf5ec61e added problem importer
blanchet
parents:
diff changeset 
     2
 
    Author:     Jasmin Blanchette, TU Muenchen
e4bccf5ec61e added problem importer
blanchet
parents:
diff changeset 
     3
 
*)
e4bccf5ec61e added problem importer
blanchet
parents:
diff changeset 
     4
 












e4bccf5ec61e
added problem importer



blanchet


parents: 

diff
changeset




     5


header {* ATP Problem Importer *}













e4bccf5ec61e
added problem importer



blanchet


parents: 

diff
changeset




     6














e4bccf5ec61e
added problem importer



blanchet


parents: 

diff
changeset




     7


theory ATP_Problem_Import













e4bccf5ec61e
added problem importer



blanchet


parents: 

diff
changeset




     8


imports Complex_Main













e4bccf5ec61e
added problem importer



blanchet


parents: 

diff
changeset




     9


uses ("atp_problem_import.ML")













e4bccf5ec61e
added problem importer



blanchet


parents: 

diff
changeset




    10


begin













e4bccf5ec61e
added problem importer



blanchet


parents: 

diff
changeset




    11














e4bccf5ec61e
added problem importer



blanchet


parents: 

diff
changeset




    12


typedecl iota (* for TPTP *)













e4bccf5ec61e
added problem importer



blanchet


parents: 

diff
changeset




    13














e4bccf5ec61e
added problem importer



blanchet


parents: 

diff
changeset




    14


use "atp_problem_import.ML"













e4bccf5ec61e
added problem importer



blanchet


parents: 

diff
changeset




    15














e4bccf5ec61e
added problem importer



blanchet


parents: 

diff
changeset




    16


end















isabelle