equal
deleted
inserted
replaced
384 |
384 |
385 fun gen_theorem kind = |
385 fun gen_theorem kind = |
386 OuterSyntax.command kind ("state " ^ kind) K.thy_goal |
386 OuterSyntax.command kind ("state " ^ kind) K.thy_goal |
387 (P.opt_locale_target -- Scan.optional (P.opt_thm_name ":" --| |
387 (P.opt_locale_target -- Scan.optional (P.opt_thm_name ":" --| |
388 Scan.ahead (P.locale_keyword || P.statement_keyword)) ("", []) -- |
388 Scan.ahead (P.locale_keyword || P.statement_keyword)) ("", []) -- |
389 P.general_statement >> (fn ((x, y), (z, w)) => |
389 P.general_statement >> (fn ((loc, a), (elems, concl)) => |
390 (Toplevel.print o Toplevel.theory_to_proof (Locale.smart_theorem kind x y z w)))); |
390 (Toplevel.print o |
|
391 Toplevel.local_theory_to_proof loc |
|
392 (Specification.theorem kind NONE (K I) a elems concl) o |
|
393 Toplevel.theory_to_proof (Locale.smart_theorem kind loc a elems concl)))); |
391 |
394 |
392 val theoremP = gen_theorem PureThy.theoremK; |
395 val theoremP = gen_theorem PureThy.theoremK; |
393 val lemmaP = gen_theorem PureThy.lemmaK; |
396 val lemmaP = gen_theorem PureThy.lemmaK; |
394 val corollaryP = gen_theorem PureThy.corollaryK; |
397 val corollaryP = gen_theorem PureThy.corollaryK; |
395 |
398 |