src/Pure/Thy/thy_output.ML
changeset 46957 0c15caf47040
parent 46950 d0181abdbdac
child 46958 0ec8f04e753a
equal deleted inserted replaced
46956:9ff441f295c2 46957:0c15caf47040
   624 end;
   624 end;
   625 
   625 
   626 
   626 
   627 (* embedded lemma *)
   627 (* embedded lemma *)
   628 
   628 
   629 val _ = Keyword.keyword "by";
   629 val _ = Keyword.declare "by" NONE;  (*overlap with command category*)
   630 
   630 
   631 val _ =
   631 val _ =
   632   Context.>> (Context.map_theory
   632   Context.>> (Context.map_theory
   633    (antiquotation (Binding.name "lemma")
   633    (antiquotation (Binding.name "lemma")
   634     (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))