src/Pure/Isar/specification.ML
changeset 45600 1bbbac9a0cb0
parent 45584 41a768a431a6
child 45601 d5178f19b671
equal deleted inserted replaced
45599:5292435af7cf 45600:1bbbac9a0cb0
    50   val type_notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
    50   val type_notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
    51   val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
    51   val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
    52   val notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
    52   val notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
    53   val theorems: string ->
    53   val theorems: string ->
    54     (Attrib.binding * (thm list * Attrib.src list) list) list ->
    54     (Attrib.binding * (thm list * Attrib.src list) list) list ->
       
    55     (binding * typ option * mixfix) list ->
    55     bool -> local_theory -> (string * thm list) list * local_theory
    56     bool -> local_theory -> (string * thm list) list * local_theory
    56   val theorems_cmd: string ->
    57   val theorems_cmd: string ->
    57     (Attrib.binding * (Facts.ref * Attrib.src list) list) list ->
    58     (Attrib.binding * (Facts.ref * Attrib.src list) list) list ->
       
    59     (binding * string option * mixfix) list ->
    58     bool -> local_theory -> (string * thm list) list * local_theory
    60     bool -> local_theory -> (string * thm list) list * local_theory
    59   val theorem: string -> Method.text option ->
    61   val theorem: string -> Method.text option ->
    60     (thm list list -> local_theory -> local_theory) -> Attrib.binding ->
    62     (thm list list -> local_theory -> local_theory) -> Attrib.binding ->
    61     Element.context_i list -> Element.statement_i ->
    63     Element.context_i list -> Element.statement_i ->
    62     bool -> local_theory -> Proof.state
    64     bool -> local_theory -> Proof.state
   281 end;
   283 end;
   282 
   284 
   283 
   285 
   284 (* fact statements *)
   286 (* fact statements *)
   285 
   287 
   286 fun gen_theorems prep_fact prep_att kind raw_facts int lthy =
   288 local
       
   289 
       
   290 fun gen_theorems prep_fact prep_att prep_vars
       
   291     kind raw_facts raw_fixes int lthy =
   287   let
   292   let
   288     val attrib = prep_att (Proof_Context.theory_of lthy);
   293     val attrib = prep_att (Proof_Context.theory_of lthy);
   289     val facts = raw_facts |> map (fn ((name, atts), bs) =>
   294     val facts = raw_facts |> map (fn ((name, atts), bs) =>
   290       ((name, map attrib atts),
   295       ((name, map attrib atts),
   291         bs |> map (fn (b, more_atts) => (prep_fact lthy b, map attrib more_atts))));
   296         bs |> map (fn (b, more_atts) => (prep_fact lthy b, map attrib more_atts))));
   292     val (res, lthy') = lthy |> Local_Theory.notes_kind kind facts;
   297     val (_, ctxt') = lthy |> prep_vars raw_fixes |-> Proof_Context.add_fixes;
       
   298 
       
   299     val facts' = facts
       
   300       |> Attrib.partial_evaluation ctxt'
       
   301       |> Element.facts_map (Element.transform_ctxt (Proof_Context.export_morphism ctxt' lthy));
       
   302     val (res, lthy') = lthy |> Local_Theory.notes_kind kind facts';
   293     val _ = Proof_Display.print_results int lthy' ((kind, ""), res);
   303     val _ = Proof_Display.print_results int lthy' ((kind, ""), res);
   294   in (res, lthy') end;
   304   in (res, lthy') end;
   295 
   305 
   296 val theorems = gen_theorems (K I) (K I);
   306 in
   297 val theorems_cmd = gen_theorems Proof_Context.get_fact Attrib.intern_src;
   307 
       
   308 val theorems = gen_theorems (K I) (K I) Proof_Context.cert_vars;
       
   309 val theorems_cmd = gen_theorems Proof_Context.get_fact Attrib.intern_src Proof_Context.read_vars;
       
   310 
       
   311 end;
   298 
   312 
   299 
   313 
   300 (* complex goal statements *)
   314 (* complex goal statements *)
   301 
   315 
   302 local
   316 local