(* 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 ‹TPTP_Parser/tptp_interpret.ML›
end
Messung V0.5 in Prozent
¤ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet am 2026-04-28)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.