equal
deleted
inserted
replaced
52 val by = Args.$$$ "by"; |
52 val by = Args.$$$ "by"; |
53 val goal = Scan.unless (by || and_) Args.name; |
53 val goal = Scan.unless (by || and_) Args.name; |
54 |
54 |
55 val _ = ML_Context.add_antiq "lemma" |
55 val _ = ML_Context.add_antiq "lemma" |
56 (fn _ => Args.context -- Args.mode "open" -- |
56 (fn _ => Args.context -- Args.mode "open" -- |
57 Scan.lift (OuterParse.and_list1 (Scan.repeat1 goal) -- |
57 Scan.lift (Parse.and_list1 (Scan.repeat1 goal) -- |
58 (by |-- Method.parse -- Scan.option Method.parse)) >> |
58 (by |-- Method.parse -- Scan.option Method.parse)) >> |
59 (fn ((ctxt, is_open), (raw_propss, methods)) => fn background => |
59 (fn ((ctxt, is_open), (raw_propss, methods)) => fn background => |
60 let |
60 let |
61 val propss = burrow (map (rpair []) o Syntax.read_props ctxt) raw_propss; |
61 val propss = burrow (map (rpair []) o Syntax.read_props ctxt) raw_propss; |
62 val i = serial (); |
62 val i = serial (); |