65 #> fold_map (augment_with_def prep_term) raw_defs); |
65 #> fold_map (augment_with_def prep_term) raw_defs); |
66 |
66 |
67 fun prep_interpretation prep_expr prep_term |
67 fun prep_interpretation prep_expr prep_term |
68 expression raw_defs initial_ctxt = |
68 expression raw_defs initial_ctxt = |
69 let |
69 let |
|
70 val _ = writeln "###-# Interpretation.prep_interpretation"; |
70 val ((propss, eq_propss, deps, eqnss, export), expr_ctxt) = prep_expr expression initial_ctxt; |
71 val ((propss, eq_propss, deps, eqnss, export), expr_ctxt) = prep_expr expression initial_ctxt; |
71 val (def_eqns, def_ctxt) = |
72 val (def_eqns, def_ctxt) = |
72 augment_with_defs prep_term raw_defs deps expr_ctxt; |
73 augment_with_defs prep_term raw_defs deps expr_ctxt; |
73 val export' = Proof_Context.export_morphism def_ctxt expr_ctxt; |
74 val export' = Proof_Context.export_morphism def_ctxt expr_ctxt; |
74 in (((propss, eq_propss, deps, eqnss, export, export'), def_eqns), def_ctxt) end; |
75 in (((propss, eq_propss, deps, eqnss, export, export'), def_eqns), def_ctxt) end; |
116 in |
117 in |
117 |
118 |
118 fun generic_interpretation prep_interpretation setup_proof note add_registration |
119 fun generic_interpretation prep_interpretation setup_proof note add_registration |
119 expression raw_defs initial_ctxt = |
120 expression raw_defs initial_ctxt = |
120 let |
121 let |
|
122 val _ = writeln "###-# Interpretation.generic_interpretation"; |
121 val (((propss, eq_propss, deps, eqnss, export, export'), def_eqns), goal_ctxt) = |
123 val (((propss, eq_propss, deps, eqnss, export, export'), def_eqns), goal_ctxt) = |
122 prep_interpretation expression raw_defs initial_ctxt; |
124 prep_interpretation expression raw_defs initial_ctxt; |
123 fun after_qed witss eqns = |
125 fun after_qed witss eqns = |
124 note_eqns_register note add_registration deps eqnss witss def_eqns eqns export export'; |
126 note_eqns_register note add_registration deps eqnss witss def_eqns eqns export export'; |
125 in setup_proof after_qed propss (flat eq_propss) goal_ctxt end; |
127 in setup_proof after_qed propss (flat eq_propss) goal_ctxt end; |
145 Attrib.local_notes Locale.add_registration_proof expression []; |
147 Attrib.local_notes Locale.add_registration_proof expression []; |
146 |
148 |
147 in |
149 in |
148 |
150 |
149 val interpret = gen_interpret cert_interpretation; |
151 val interpret = gen_interpret cert_interpretation; |
|
152 val interpret = |
|
153 (writeln "###-# Interpretation.interpret"; |
|
154 gen_interpret cert_interpretation); |
|
155 |
150 val interpret_cmd = gen_interpret read_interpretation; |
156 val interpret_cmd = gen_interpret read_interpretation; |
|
157 val interpret_cmd = |
|
158 (writeln "###-# Interpretation.interpret_cmd"; |
|
159 gen_interpret read_interpretation); |
151 |
160 |
152 end; |
161 end; |
153 |
162 |
154 |
163 |
155 (* interpretation in local theories *) |
164 (* interpretation in local theories *) |