| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/C/Firefox/widget/tests/ (Firefox Browser Version 153.0.1©) Datei vom 27.6.2026 mit Größe 51 kB |
|
Quelle Import_Setup.thy Sprache: Isabelle |
|||||||||||||||
|
(* 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
¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet am 2026-09-29) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-10-10