95 |
95 |
96 val _ = |
96 val _ = |
97 Theory.setup (Attrib.setup \<^binding>\<open>import_const\<close> |
97 Theory.setup (Attrib.setup \<^binding>\<open>import_const\<close> |
98 (Scan.lift Parse.name -- |
98 (Scan.lift Parse.name -- |
99 Scan.option (Scan.lift \<^keyword>\<open>:\<close> |-- Args.const {proper = true, strict = false}) >> |
99 Scan.option (Scan.lift \<^keyword>\<open>:\<close> |-- Args.const {proper = true, strict = false}) >> |
100 (fn (s1, s2) => Thm.declaration_attribute |
100 (fn (c, d) => Thm.declaration_attribute |
101 (fn th => Context.mapping (add_const_def s1 th s2) I))) |
101 (fn th => Context.mapping (add_const_def c th d) I))) |
102 "declare a theorem as an equality that maps the given constant") |
102 "declare a theorem as an equality that maps the given constant") |
103 |
103 |
104 val _ = |
104 val _ = |
105 Theory.setup (Attrib.setup \<^binding>\<open>import_type\<close> |
105 Theory.setup (Attrib.setup \<^binding>\<open>import_type\<close> |
106 (Scan.lift (Parse.name -- Parse.name -- Parse.name) >> |
106 (Scan.lift (Parse.name -- Parse.name -- Parse.name) >> |
107 (fn ((tyname, absname), repname) => Thm.declaration_attribute |
107 (fn ((c, abs), rep) => Thm.declaration_attribute |
108 (fn th => Context.mapping (add_typ_def tyname absname repname th) I))) |
108 (fn th => Context.mapping (add_typ_def c abs rep th) I))) |
109 "declare a type_definition theorem as a map for an imported type with abs and rep") |
109 "declare a type_definition theorem as a map for an imported type with abs and rep") |
110 |
110 |
111 val _ = |
111 val _ = |
112 Outer_Syntax.command \<^command_keyword>\<open>import_type_map\<close> |
112 Outer_Syntax.command \<^command_keyword>\<open>import_type_map\<close> |
113 "map external type name to existing Isabelle/HOL type name" |
113 "map external type name to existing Isabelle/HOL type name" |