equal
deleted
inserted
replaced
294 |
294 |
295 (* statements *) |
295 (* statements *) |
296 |
296 |
297 val statement = P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.propp); |
297 val statement = P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.propp); |
298 val long_statement = |
298 val long_statement = |
299 Scan.repeat P.locale_element -- (P.$$$ "shows" |-- statement) || statement >> pair []; |
299 statement >> pair [] || Scan.repeat P.locale_element -- (P.$$$ "shows" |-- statement); |
300 |
300 |
301 fun gen_theorem k = |
301 fun gen_theorem k = |
302 OuterSyntax.command k ("state " ^ k) K.thy_goal |
302 OuterSyntax.command k ("state " ^ k) K.thy_goal |
303 (Scan.optional (P.thm_name ":" --| |
303 (Scan.optional (P.thm_name ":" --| |
304 Scan.ahead (P.$$$ "(" || P.locale_keyword || P.$$$ "shows")) ("", []) |
304 Scan.ahead (P.$$$ "(" || P.locale_keyword || P.$$$ "shows")) ("", []) |