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/ROOT.ML
author blanchet
Wed, 11 Jul 2012 21:43:19 +0200
changeset 48250 1065c307fafe
parent 48234 06216c789ac9
child 48284 a3cb8901d60c
permissions -rw-r--r--
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
43804
eb9be23db2b7 cleanly separate TPTP related files from other examples
blanchet
parents:
diff changeset 
     1
 
(*  Title:      HOL/TPTP/ROOT.ML
eb9be23db2b7 cleanly separate TPTP related files from other examples
blanchet
parents:
diff changeset 
     2
 
    Author:     Jasmin Blanchette, TU Muenchen
eb9be23db2b7 cleanly separate TPTP related files from other examples
blanchet
parents:
diff changeset 
     3
 
    Author:     Nik Sultana, University of Cambridge
eb9be23db2b7 cleanly separate TPTP related files from other examples
blanchet
parents:
diff changeset 
     4
 
    Copyright   2011
eb9be23db2b7 cleanly separate TPTP related files from other examples
blanchet
parents:
diff changeset 
     5
 












eb9be23db2b7
cleanly separate TPTP related files from other examples



blanchet


parents: 

diff
changeset




     6


TPTP-related extensions.













eb9be23db2b7
cleanly separate TPTP related files from other examples



blanchet


parents: 

diff
changeset




     7


*)













eb9be23db2b7
cleanly separate TPTP related files from other examples



blanchet


parents: 

diff
changeset




     8














eb9be23db2b7
cleanly separate TPTP related files from other examples



blanchet


parents: 

diff
changeset




     9


use_thys [








48234






06216c789ac9
moved MaSh into own files



blanchet


parents: 
47792

diff
changeset




    10


  "MaSh_Import",








47792






804fdf0f6006
get rid of old CASC setup and move the arithmetic part to a new theory



blanchet


parents: 
47526

diff
changeset




    11


  "TPTP_Interpret",













804fdf0f6006
get rid of old CASC setup and move the arithmetic part to a new theory



blanchet


parents: 
47526

diff
changeset




    12


  "THF_Arith"








43804






eb9be23db2b7
cleanly separate TPTP related files from other examples



blanchet


parents: 

diff
changeset




    13


];













eb9be23db2b7
cleanly separate TPTP related files from other examples



blanchet


parents: 

diff
changeset




    14














eb9be23db2b7
cleanly separate TPTP related files from other examples



blanchet


parents: 

diff
changeset




    15


Unsynchronized.setmp Proofterm.proofs (!Proofterm.proofs)








47792






804fdf0f6006
get rid of old CASC setup and move the arithmetic part to a new theory



blanchet


parents: 
47526

diff
changeset




    16


  use_thy "ATP_Problem_Import";















isabelle