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 haftmann
Fri, 15 Feb 2013 08:31:31 +0100
changeset 51143 0a2371e7ced3
parent 48891 c0eafbd55de3
child 57796 07521fed6071
permissions -rw-r--r--
two target language numeral types: integer and natural, as replacement for code_numeral; former theory HOL/Library/Code_Numeral_Types replaces HOL/Code_Numeral; refined stack of theories implementing int and/or nat by target language numerals; reduced number of target language numeral types to exactly one
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








48891






c0eafbd55de3
prefer ML_file over old uses;



wenzelm


parents: 
47519

diff
changeset




    11


begin













c0eafbd55de3
prefer ML_file over old uses;



wenzelm


parents: 
47519

diff
changeset




    12














c0eafbd55de3
prefer ML_file over old uses;



wenzelm


parents: 
47519

diff
changeset




    13


typedecl "ind"








47509






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



sultana


parents: 

diff
changeset




    14









48891






c0eafbd55de3
prefer ML_file over old uses;



wenzelm


parents: 
47519

diff
changeset




    15


ML_file  "TPTP_Parser/tptp_interpret.ML"













c0eafbd55de3
prefer ML_file over old uses;



wenzelm


parents: 
47519

diff
changeset




    16









47509






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



sultana


parents: 

diff
changeset




    17


end














isabelle