equal
deleted
inserted
replaced
74 |
74 |
75 fun lift_morphism thy f = |
75 fun lift_morphism thy f = |
76 let |
76 let |
77 fun term t = Thm.term_of (Drule.cterm_rule f (Thm.cterm_of thy t)) |
77 fun term t = Thm.term_of (Drule.cterm_rule f (Thm.cterm_of thy t)) |
78 in |
78 in |
79 Morphism.thm_morphism f $> Morphism.term_morphism term |
79 Morphism.morphism "lift_morphism" |
80 $> Morphism.typ_morphism (Logic.type_map term) |
80 {binding = [], |
|
81 typ = [Logic.type_map term], |
|
82 term = [term], |
|
83 fact = [map f]} |
81 end |
84 end |
82 |
85 |
83 fun import_function_data t ctxt = |
86 fun import_function_data t ctxt = |
84 let |
87 let |
85 val thy = Proof_Context.theory_of ctxt |
88 val thy = Proof_Context.theory_of ctxt |