(* Title: HOL/Import/Import_Setup.thy
Author: Cezary Kaliszyk, University of Innsbruck
Author: Alexander Krauss, QAware GmbH
*)
section \<open>Importer machinery and required theorems\<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>
lemma light_ex_imp_nonempty:
"P t \ \x. x \ Collect P"
by auto
lemma typedef_hol2hollight:
assumes a: "type_definition Rep Abs (Collect P)"
shows "Abs (Rep a) = a \ P r = (Rep (Abs r) = r)"
by (metis type_definition.Rep_inverse type_definition.Abs_inverse
type_definition.Rep a mem_Collect_eq)
lemma ext2:
"(\x. f x = g x) \ f = g"
by auto
ML_file \<open>import_rule.ML\<close>
end
¤ Dauer der Verarbeitung: 0.18 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
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.
|
