src/Pure/Isar/isar_cmd.ML
changeset 5880 feec44106a8e
parent 5831 996361157cfb
child 5895 457b42674b57
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Mon Nov 16 11:03:35 1998 +0100
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Mon Nov 16 11:04:35 1998 +0100
     1.3 @@ -20,11 +20,12 @@
     1.4    val load: string -> Toplevel.transition -> Toplevel.transition
     1.5    val print_theory: Toplevel.transition -> Toplevel.transition
     1.6    val print_syntax: Toplevel.transition -> Toplevel.transition
     1.7 +  val print_theorems: Toplevel.transition -> Toplevel.transition
     1.8    val print_attributes: Toplevel.transition -> Toplevel.transition
     1.9    val print_methods: Toplevel.transition -> Toplevel.transition
    1.10    val print_binds: Toplevel.transition -> Toplevel.transition
    1.11    val print_lthms: Toplevel.transition -> Toplevel.transition
    1.12 -  val print_thms: xstring -> Toplevel.transition -> Toplevel.transition
    1.13 +  val print_thms: xstring * Args.src list -> Toplevel.transition -> Toplevel.transition
    1.14    val print_prop: string -> Toplevel.transition -> Toplevel.transition
    1.15    val print_term: string -> Toplevel.transition -> Toplevel.transition
    1.16    val print_type: string -> Toplevel.transition -> Toplevel.transition
    1.17 @@ -81,6 +82,7 @@
    1.18  
    1.19  val print_theory = Toplevel.keep (PureThy.print_theory o Toplevel.theory_of);
    1.20  val print_syntax = Toplevel.keep (Display.print_syntax o Toplevel.theory_of);
    1.21 +val print_theorems = Toplevel.keep (PureThy.print_theorems o Toplevel.theory_of);
    1.22  val print_attributes = Toplevel.keep (Attrib.print_attributes o Toplevel.theory_of);
    1.23  val print_methods = Toplevel.keep (Method.print_methods o Toplevel.theory_of);
    1.24  
    1.25 @@ -93,16 +95,24 @@
    1.26  
    1.27  (* print theorems *)
    1.28  
    1.29 -fun print_thms name = Toplevel.keep (fn state =>
    1.30 +fun global_attribs thy ths srcs =
    1.31 +  #2 (Attribute.applys ((Theory.copy thy, ths), map (Attrib.global_attribute thy) srcs));
    1.32 +
    1.33 +fun local_attribs st ths srcs =
    1.34 +  #2 (Attribute.applys ((Proof.context_of st, ths),
    1.35 +    map (Attrib.local_attribute (Proof.theory_of st)) srcs));
    1.36 +
    1.37 +fun print_thms (name, srcs) = Toplevel.keep (fn state =>
    1.38    let
    1.39      val prt_tthm = Attribute.pretty_tthm;
    1.40      fun prt_tthms [th] = prt_tthm th
    1.41        | prt_tthms ths = Pretty.block (Pretty.fbreaks (map prt_tthm ths));
    1.42  
    1.43 -    val tthms = map (apfst (Thm.transfer (Toplevel.theory_of state)))
    1.44 +    val ths = map (apfst (Thm.transfer (Toplevel.theory_of state)))
    1.45        (Toplevel.node_cases PureThy.get_tthms (ProofContext.get_tthms o Proof.context_of)
    1.46          state name);
    1.47 -  in Pretty.writeln (prt_tthms tthms) end);
    1.48 +    val ths' = Toplevel.node_cases global_attribs local_attribs state ths srcs;
    1.49 +  in Pretty.writeln (prt_tthms ths') end);
    1.50  
    1.51  
    1.52  (* print types, terms and props *)