src/Pure/Isar/proof.ML
changeset 6982 4d2a3f35af93
parent 6950 ab6d35b7283f
child 6996 1a28d968c5aa
     1.1 --- a/src/Pure/Isar/proof.ML	Mon Jul 12 22:27:20 1999 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Mon Jul 12 22:27:51 1999 +0200
     1.3 @@ -22,6 +22,8 @@
     1.4    val assert_forward: state -> state
     1.5    val assert_backward: state -> state
     1.6    val enter_forward: state -> state
     1.7 +  val show_hyps: bool ref
     1.8 +  val pretty_thm: thm -> Pretty.T
     1.9    val verbose: bool ref
    1.10    val print_state: state -> unit
    1.11    val level: state -> int
    1.12 @@ -70,8 +72,8 @@
    1.13    val have_i: string -> context attribute list -> term * (term list * term list)
    1.14      -> state -> state
    1.15    val at_bottom: state -> bool
    1.16 -  val local_qed: (state -> state Seq.seq) -> ({kind: string, name: string, thm: thm} -> unit)
    1.17 -    -> state -> state Seq.seq
    1.18 +  val local_qed: (state -> state Seq.seq)
    1.19 +    -> ({kind: string, name: string, thm: thm} -> unit) * (thm -> unit) -> state -> state Seq.seq
    1.20    val global_qed: (state -> state Seq.seq) -> state
    1.21      -> (theory * {kind: string, name: string, thm: thm}) Seq.seq
    1.22    val begin_block: state -> state
    1.23 @@ -280,11 +282,14 @@
    1.24  
    1.25  (** print_state **)
    1.26  
    1.27 +val show_hyps = ProofContext.show_hyps;
    1.28 +val pretty_thm = ProofContext.pretty_thm;
    1.29 +
    1.30  val verbose = ProofContext.verbose;
    1.31  
    1.32  fun print_facts _ None = ()
    1.33 -  | print_facts s (Some ths) = Pretty.writeln (Pretty.big_list (s ^ " facts:")
    1.34 -      (map Display.pretty_thm_no_hyps ths));
    1.35 +  | print_facts s (Some ths) =
    1.36 +      Pretty.writeln (Pretty.big_list (s ^ " facts:") (map pretty_thm ths));
    1.37  
    1.38  fun print_state (state as State ({context, facts, mode, goal = _}, nodes)) =
    1.39    let
    1.40 @@ -395,11 +400,12 @@
    1.41  fun RANGE [] _ = all_tac
    1.42    | RANGE (tac :: tacs) i = RANGE tacs (i + 1) THEN tac i;
    1.43  
    1.44 -fun export_goal raw_rule inner state =
    1.45 +fun export_goal print_rule raw_rule inner state =
    1.46    let
    1.47      val (outer, (_, (result, (facts, thm)))) = find_goal 0 state;
    1.48      val (exp, tacs) = export_wrt inner (Some outer);
    1.49      val rule = exp raw_rule;
    1.50 +    val _ = print_rule rule;
    1.51      val thmq = FIRSTGOAL (Tactic.rtac rule THEN' RANGE (map #1 tacs)) thm;
    1.52    in Seq.map (fn th => map_goal (K (result, (facts, th))) state) thmq end;
    1.53  
    1.54 @@ -639,13 +645,13 @@
    1.55  
    1.56  (* local_qed *)
    1.57  
    1.58 -fun finish_local print_result state =
    1.59 +fun finish_local (print_result, print_rule) state =
    1.60    let
    1.61      val (ctxt, ((kind, name, t), (_, raw_thm))) = current_goal state;
    1.62      val result = prep_result state t raw_thm;
    1.63      val (atts, opt_solve) =
    1.64        (case kind of
    1.65 -        Goal atts => (atts, export_goal result ctxt)
    1.66 +        Goal atts => (atts, export_goal print_rule result ctxt)
    1.67        | Aux atts => (atts, Seq.single)
    1.68        | _ => err_malformed "finish_local" state);
    1.69    in
    1.70 @@ -657,11 +663,11 @@
    1.71      |> opt_solve
    1.72    end;
    1.73  
    1.74 -fun local_qed finalize print_result state =
    1.75 +fun local_qed finalize print state =
    1.76    state
    1.77    |> end_proof false
    1.78    |> finalize
    1.79 -  |> (Seq.flat o Seq.map (finish_local print_result));
    1.80 +  |> (Seq.flat o Seq.map (finish_local print));
    1.81  
    1.82  
    1.83  (* global_qed *)