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
Tue, 10 Jul 2012 23:36:03 +0200
changeset 48234 06216c789ac9
parent 47792 804fdf0f6006
child 48250 1065c307fafe
permissions -rw-r--r--
moved MaSh into own files
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 [








46844






5d9aab0c609c
added tptp parser;



sultana


parents: 
46324

diff
changeset




    10


  "ATP_Theory_Export",








48234






06216c789ac9
moved MaSh into own files



blanchet


parents: 
47792

diff
changeset




    11


  "MaSh_Import",








47792






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



blanchet


parents: 
47526

diff
changeset




    12


  "TPTP_Interpret",













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



blanchet


parents: 
47526

diff
changeset




    13


  "THF_Arith"








43804






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














eb9be23db2b7
cleanly separate TPTP related files from other examples



blanchet


parents: 

diff
changeset




    16


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




    17


  use_thy "ATP_Problem_Import";















isabelle