src/Pure/Pure.thy
changeset 63094 056ea294c256
parent 63064 2f18172214c8
child 63178 b9e1d53124f5
     1.1 --- a/src/Pure/Pure.thy	Sat May 14 13:52:01 2016 +0200
     1.2 +++ b/src/Pure/Pure.thy	Sat May 14 19:49:10 2016 +0200
     1.3 @@ -397,6 +397,38 @@
     1.4  ML \<open>
     1.5  local
     1.6  
     1.7 +val long_keyword =
     1.8 +  Parse_Spec.includes >> K "" ||
     1.9 +  Parse_Spec.long_statement_keyword;
    1.10 +
    1.11 +val long_statement =
    1.12 +  Scan.optional (Parse_Spec.opt_thm_name ":" --| Scan.ahead long_keyword) Attrib.empty_binding --
    1.13 +  Scan.optional Parse_Spec.includes [] -- Parse_Spec.long_statement
    1.14 +    >> (fn ((binding, includes), (elems, concl)) => (true, binding, includes, elems, concl));
    1.15 +
    1.16 +val short_statement =
    1.17 +  Parse_Spec.statement -- Parse_Spec.if_statement -- Parse.for_fixes
    1.18 +    >> (fn ((shows, assumes), fixes) =>
    1.19 +      (false, Attrib.empty_binding, [], [Element.Fixes fixes, Element.Assumes assumes],
    1.20 +        Element.Shows shows));
    1.21 +
    1.22 +fun theorem spec schematic descr =
    1.23 +  Outer_Syntax.local_theory_to_proof' spec ("state " ^ descr)
    1.24 +    ((long_statement || short_statement) >> (fn (long, binding, includes, elems, concl) =>
    1.25 +      ((if schematic then Specification.schematic_theorem_cmd else Specification.theorem_cmd)
    1.26 +        long Thm.theoremK NONE (K I) binding includes elems concl)));
    1.27 +
    1.28 +val _ = theorem @{command_keyword theorem} false "theorem";
    1.29 +val _ = theorem @{command_keyword lemma} false "lemma";
    1.30 +val _ = theorem @{command_keyword corollary} false "corollary";
    1.31 +val _ = theorem @{command_keyword proposition} false "proposition";
    1.32 +val _ = theorem @{command_keyword schematic_goal} true "schematic goal";
    1.33 +
    1.34 +in end\<close>
    1.35 +
    1.36 +ML \<open>
    1.37 +local
    1.38 +
    1.39  val _ =
    1.40    Outer_Syntax.local_theory' @{command_keyword lemmas} "define theorems"
    1.41      (Parse_Spec.name_facts -- Parse.for_fixes >>
    1.42 @@ -639,24 +671,6 @@
    1.43    Parse_Spec.statement -- Parse_Spec.cond_statement -- Parse.for_fixes
    1.44      >> (fn ((shows, (strict, assumes)), fixes) => (strict, fixes, assumes, shows));
    1.45  
    1.46 -fun theorem spec schematic descr =
    1.47 -  Outer_Syntax.local_theory_to_proof' spec
    1.48 -    ("state " ^ descr)
    1.49 -    (Scan.optional (Parse_Spec.opt_thm_name ":" --|
    1.50 -      Scan.ahead (Parse_Spec.includes >> K "" ||
    1.51 -        Parse_Spec.locale_keyword || Parse_Spec.statement_keyword)) Attrib.empty_binding --
    1.52 -      Scan.optional Parse_Spec.includes [] --
    1.53 -      Parse_Spec.general_statement >> (fn ((a, includes), (elems, concl)) =>
    1.54 -        ((if schematic then Specification.schematic_theorem_cmd else Specification.theorem_cmd)
    1.55 -          Thm.theoremK NONE (K I) a includes elems concl)));
    1.56 -
    1.57 -val _ = theorem @{command_keyword theorem} false "theorem";
    1.58 -val _ = theorem @{command_keyword lemma} false "lemma";
    1.59 -val _ = theorem @{command_keyword corollary} false "corollary";
    1.60 -val _ = theorem @{command_keyword proposition} false "proposition";
    1.61 -val _ = theorem @{command_keyword schematic_goal} true "schematic goal";
    1.62 -
    1.63 -
    1.64  val _ =
    1.65    Outer_Syntax.command @{command_keyword have} "state local goal"
    1.66      (structured_statement >> (fn (a, b, c, d) =>