equal
deleted
inserted
replaced
624 end; |
624 end; |
625 |
625 |
626 |
626 |
627 (* embedded lemma *) |
627 (* embedded lemma *) |
628 |
628 |
|
629 val _ = Keyword.keyword "by"; |
|
630 |
629 val _ = |
631 val _ = |
630 Context.>> (Context.map_theory |
632 Context.>> (Context.map_theory |
631 (antiquotation (Binding.name "lemma") |
633 (antiquotation (Binding.name "lemma") |
632 (Args.prop -- Scan.lift (Args.$$$ "by" |-- Method.parse -- Scan.option Method.parse)) |
634 (Args.prop -- Scan.lift (Args.$$$ "by" |-- Method.parse -- Scan.option Method.parse)) |
633 (fn {source, context, ...} => fn (prop, methods) => |
635 (fn {source, context, ...} => fn (prop, methods) => |