equal
deleted
inserted
replaced
383 Method.intros_tac |
383 Method.intros_tac |
384 (Witnesses.get ctxt @ Intros.get ctxt @ (if eager then Unfolds.get ctxt else [])) facts st; |
384 (Witnesses.get ctxt @ Intros.get ctxt @ (if eager then Unfolds.get ctxt else [])) facts st; |
385 |
385 |
386 val _ = Context.>> (Context.map_theory |
386 val _ = Context.>> (Context.map_theory |
387 (Method.add_methods |
387 (Method.add_methods |
388 [("new_intro_locales", |
388 [("intro_locales", |
389 Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac false ctxt)), |
389 Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac false ctxt ORELSE' |
|
390 Locale.intro_locales_tac false ctxt)), |
390 "back-chain introduction rules of locales without unfolding predicates"), |
391 "back-chain introduction rules of locales without unfolding predicates"), |
391 ("new_unfold_locales", |
392 ("unfold_locales", |
392 Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac true ctxt)), |
393 Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac true ctxt ORELSE' |
|
394 Locale.intro_locales_tac true ctxt)), |
393 "back-chain all introduction rules of locales")])); |
395 "back-chain all introduction rules of locales")])); |
394 |
396 |
395 |
397 |
396 end; |
398 end; |
397 |
399 |