equal
deleted
inserted
replaced
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 ((loc, a), (elems, concl)) => |
389 P.general_statement >> (fn ((loc, a), (elems, concl)) => |
390 (Toplevel.print o |
390 (Toplevel.print o |
391 Toplevel.local_theory_to_proof loc |
391 Toplevel.local_theory_to_proof loc |
392 (Specification.theorem kind NONE (K I) a elems concl) o |
392 (Specification.theorem kind NONE (K I) a elems concl)))); |
393 Toplevel.theory_to_proof (Locale.smart_theorem kind loc a elems concl)))); |
|
394 |
393 |
395 val theoremP = gen_theorem PureThy.theoremK; |
394 val theoremP = gen_theorem PureThy.theoremK; |
396 val lemmaP = gen_theorem PureThy.lemmaK; |
395 val lemmaP = gen_theorem PureThy.lemmaK; |
397 val corollaryP = gen_theorem PureThy.corollaryK; |
396 val corollaryP = gen_theorem PureThy.corollaryK; |
398 |
397 |