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/TPTP_Interpret.thy
author wenzelm
Sun, 20 May 2012 11:34:33 +0200
changeset 47884 21c42b095c84
parent 47519 9c3acd90063a
child 48891 c0eafbd55de3
permissions -rw-r--r--
try to avoid races again (cf. 8c37cb84065f and fd3a36e48b09);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
47509
6f215c2ebd72 split TPTP_Parser thy -- parser can rely on smaller image, whereas TPTP_Interpret requires HOL;
sultana
parents:
diff changeset 
     1
 
(*  Title:      HOL/TPTP/TPTP_Interpret.thy
6f215c2ebd72 split TPTP_Parser thy -- parser can rely on smaller image, whereas TPTP_Interpret requires HOL;
sultana
parents:
diff changeset 
     2
 
    Author:     Nik Sultana, Cambridge University Computer Laboratory
6f215c2ebd72 split TPTP_Parser thy -- parser can rely on smaller image, whereas TPTP_Interpret requires HOL;
sultana
parents:
diff changeset 
     3
 












6f215c2ebd72
split TPTP_Parser thy -- parser can rely on smaller image, whereas TPTP_Interpret requires HOL;



sultana


parents: 

diff
changeset




     4


Importing TPTP files into Isabelle/HOL: parsing TPTP formulas and













6f215c2ebd72
split TPTP_Parser thy -- parser can rely on smaller image, whereas TPTP_Interpret requires HOL;



sultana


parents: 

diff
changeset




     5


interpreting them as HOL terms (i.e. importing types and type-checking the terms)













6f215c2ebd72
split TPTP_Parser thy -- parser can rely on smaller image, whereas TPTP_Interpret requires HOL;



sultana


parents: 

diff
changeset




     6


*)













6f215c2ebd72
split TPTP_Parser thy -- parser can rely on smaller image, whereas TPTP_Interpret requires HOL;



sultana


parents: 

diff
changeset




     7














6f215c2ebd72
split TPTP_Parser thy -- parser can rely on smaller image, whereas TPTP_Interpret requires HOL;



sultana


parents: 

diff
changeset




     8


theory TPTP_Interpret













6f215c2ebd72
split TPTP_Parser thy -- parser can rely on smaller image, whereas TPTP_Interpret requires HOL;



sultana


parents: 

diff
changeset




     9


imports Main TPTP_Parser













6f215c2ebd72
split TPTP_Parser thy -- parser can rely on smaller image, whereas TPTP_Interpret requires HOL;



sultana


parents: 

diff
changeset




    10


keywords "import_tptp" :: thy_decl








47519






9c3acd90063a
simplified interpretation of '$i';



sultana


parents: 
47509

diff
changeset




    11


uses  ("TPTP_Parser/tptp_interpret.ML")








47509






6f215c2ebd72
split TPTP_Parser thy -- parser can rely on smaller image, whereas TPTP_Interpret requires HOL;



sultana


parents: 

diff
changeset




    12














6f215c2ebd72
split TPTP_Parser thy -- parser can rely on smaller image, whereas TPTP_Interpret requires HOL;



sultana


parents: 

diff
changeset




    13


begin








47519






9c3acd90063a
simplified interpretation of '$i';



sultana


parents: 
47509

diff
changeset




    14


typedecl "ind"













9c3acd90063a
simplified interpretation of '$i';



sultana


parents: 
47509

diff
changeset




    15


use  "TPTP_Parser/tptp_interpret.ML"








47509






6f215c2ebd72
split TPTP_Parser thy -- parser can rely on smaller image, whereas TPTP_Interpret requires HOL;



sultana


parents: 

diff
changeset




    16


end














isabelle