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.10 Sekunden
(vorverarbeitet am 2026-06-29)
¤
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.
