equal
deleted
inserted
replaced
227 val distinct_thm = Proof_Context.get_thm ctxt dist_thm_name; |
227 val distinct_thm = Proof_Context.get_thm ctxt dist_thm_name; |
228 val rule = DistinctTreeProver.distinct_implProver ctxt distinct_thm goal; |
228 val rule = DistinctTreeProver.distinct_implProver ctxt distinct_thm goal; |
229 in resolve_tac ctxt [rule] i end); |
229 in resolve_tac ctxt [rule] i end); |
230 |
230 |
231 fun tac ctxt = |
231 fun tac ctxt = |
232 Locale.intro_locales_tac true ctxt [] THEN ALLGOALS (solve_tac ctxt); |
232 Locale.intro_locales_tac {strict = true, eager = true} ctxt [] THEN ALLGOALS (solve_tac ctxt); |
233 |
233 |
234 in |
234 in |
235 thy |> prove_interpretation_in tac (name, parent_expr) |
235 thy |> prove_interpretation_in tac (name, parent_expr) |
236 end; |
236 end; |
237 |
237 |
364 |
364 |
365 fun interprete_parent (prefix, (_, pname, rs)) = |
365 fun interprete_parent (prefix, (_, pname, rs)) = |
366 let |
366 let |
367 val expr = ([(pname, (prefix, (Expression.Positional rs,[])))],[]) |
367 val expr = ([(pname, (prefix, (Expression.Positional rs,[])))],[]) |
368 in prove_interpretation_in |
368 in prove_interpretation_in |
369 (fn ctxt => Locale.intro_locales_tac false ctxt []) |
369 (fn ctxt => Locale.intro_locales_tac {strict = true, eager = false} ctxt []) |
370 (full_name, expr) end; |
370 (full_name, expr) end; |
371 |
371 |
372 fun declare_declinfo updates lthy phi ctxt = |
372 fun declare_declinfo updates lthy phi ctxt = |
373 let |
373 let |
374 fun upd_prf ctxt = |
374 fun upd_prf ctxt = |