(* Title: HOL/Import/Import_Setup.thy Author: Cezary Kaliszyk, University of Innsbruck Author: Alexander Krauss, QAware GmbH Author: Makarius *)
section‹Importer machinery›
theory Import_Setup imports Main
keywords "import_type_map""import_const_map""import_file" :: thy_decl begin
ML_file ‹import_data.ML›
text‹ Initial type and constant maps, for types and constants that are not defined, which means their definitions do not appear in the proof dump. ›
import_type_map bool : bool
import_type_map "fun" : "fun"
import_type_map ind : ind
import_const_map "=" : HOL.eq
import_const_map "@" : Eps
ML_file ‹import_rule.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.
