Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/HOL/Metis_Examples/   (Beweissystem Isabelle Version 2025-1©)  Datei vom 16.11.2025 mit Größe 6 kB image not shown  

Impressum TPTP_Interpret.thy   Interaktion und
Portierbarkeitunbekannt

 
(*  Title:      HOL/TPTP/TPTP_Interpret.thy
    Author:     Nik Sultana, Cambridge University Computer Laboratory

Importing TPTP files into Isabelle/HOL: parsing TPTP formulas and
interpreting them as HOL terms (i.e. importing types and type-checking the terms)
*)


theory TPTP_Interpret
imports Complex_Main TPTP_Parser
keywords "import_tptp" :: thy_decl
begin

typedecl ind

ML_file \<open>TPTP_Parser/tptp_interpret.ML\<close>

end

100%


[ Seitenstruktur0.3Drucken  etwas mehr zur Ethik  ]