(* Title: HOL/Import/Import_Setup.thy Author: Cezary Kaliszyk, University of Innsbruck Author: Alexander Krauss, QAware GmbH Author: Makarius
*)
section \<open>Importer machinery\<close>
theory Import_Setup imports Main
keywords "import_type_map""import_const_map""import_file" :: thy_decl begin
ML_file \<open>import_data.ML\<close>
text\<open>
Initial type and constant maps, fortypesand constants that are not
defined, which means their definitions do not appear in the proof dump. \<close>
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 \<open>import_rule.ML\<close>
end
¤ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
¤
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 ist noch experimentell.
