removed the_fact;
authorwenzelm
Wed Sep 01 21:11:44 1999 +0200 (1999-09-01)
changeset 741235ebe1452c10
parent 7411 4dbff71ac480
child 7413 e25ad9ab0b50
removed the_fact;
added pretty_thms;
fix: common constraints;
renamed "facts" to "this";
print_state: tuned "Using facts";
src/Pure/Isar/proof.ML
     1.1 --- a/src/Pure/Isar/proof.ML	Wed Sep 01 21:10:05 1999 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Wed Sep 01 21:11:44 1999 +0200
     1.3 @@ -16,7 +16,6 @@
     1.4    val theory_of: state -> theory
     1.5    val sign_of: state -> Sign.sg
     1.6    val the_facts: state -> thm list
     1.7 -  val the_fact: state -> thm
     1.8    val get_goal: state -> thm list * thm
     1.9    val goal_facts: (state -> thm list) -> state -> state
    1.10    val use_facts: state -> state
    1.11 @@ -26,6 +25,7 @@
    1.12    val enter_forward: state -> state
    1.13    val show_hyps: bool ref
    1.14    val pretty_thm: thm -> Pretty.T
    1.15 +  val pretty_thms: thm list -> Pretty.T
    1.16    val verbose: bool ref
    1.17    val print_state: int -> state -> unit
    1.18    val level: state -> int
    1.19 @@ -40,8 +40,8 @@
    1.20    val have_thmss: thm list -> string -> context attribute list ->
    1.21      (thm list * context attribute list) list -> state -> state
    1.22    val simple_have_thms: string -> thm list -> state -> state
    1.23 -  val fix: (string * string option) list -> state -> state
    1.24 -  val fix_i: (string * typ) list -> state -> state
    1.25 +  val fix: (string list * string option) list -> state -> state
    1.26 +  val fix_i: (string list * typ) list -> state -> state
    1.27    val assm: (int -> tactic) * (int -> tactic)
    1.28      -> (string * context attribute list * (string * (string list * string list)) list) list
    1.29      -> state -> state
    1.30 @@ -191,18 +191,13 @@
    1.31  fun the_facts (State (Node {facts = Some facts, ...}, _)) = facts
    1.32    | the_facts state = raise STATE ("No current facts available", state);
    1.33  
    1.34 -fun the_fact state =
    1.35 -  (case the_facts state of
    1.36 -    [fact] => fact
    1.37 -  | _ => raise STATE ("Single fact expected", state));
    1.38 -
    1.39  fun assert_facts state = (the_facts state; state);
    1.40  fun get_facts (State (Node {facts, ...}, _)) = facts;
    1.41  
    1.42  fun put_facts facts state =
    1.43    state
    1.44    |> map_current (fn (ctxt, _, mode, goal) => (ctxt, facts, mode, goal))
    1.45 -  |> put_thms ("facts", if_none facts []);
    1.46 +  |> put_thms ("this", if_none facts []);
    1.47  
    1.48  val reset_facts = put_facts None;
    1.49  
    1.50 @@ -288,6 +283,10 @@
    1.51  val show_hyps = ProofContext.show_hyps;
    1.52  val pretty_thm = ProofContext.pretty_thm;
    1.53  
    1.54 +fun pretty_thms [th] = pretty_thm th
    1.55 +  | pretty_thms ths = Pretty.block (Pretty.fbreaks (map pretty_thm ths));
    1.56 +
    1.57 +
    1.58  val verbose = ProofContext.verbose;
    1.59  
    1.60  fun print_facts _ None = ()
    1.61 @@ -303,7 +302,8 @@
    1.62        | levels_up i = " (" ^ string_of_int i ^ " levels up)";
    1.63  
    1.64      fun print_goal (_, (i, (((kind, name, _), (goal_facts, thm)), _))) =
    1.65 -      (print_facts "Using" (if null goal_facts then None else Some goal_facts);
    1.66 +      (print_facts "Using"
    1.67 +          (if mode <> Backward orelse null goal_facts then None else Some goal_facts);
    1.68          writeln (kind_name kind ^ " " ^ quote name ^ levels_up (i div 2) ^ ":");
    1.69          Locale.print_goals_marker begin_goal (! goals_limit) thm);
    1.70  
    1.71 @@ -587,7 +587,6 @@
    1.72        state
    1.73        |> assert_forward_or_chain
    1.74        |> enter_forward
    1.75 -      |> opt_block
    1.76        |> map_context_result (fn c => prepp (c, raw_propp));
    1.77      val cprop = Thm.cterm_of (sign_of state') prop;
    1.78      val casms = map #1 (assumptions state');
    1.79 @@ -597,6 +596,7 @@
    1.80      val goal = foldr cut_asm (casms, Drule.mk_triv_goal cprop);
    1.81    in
    1.82      state'
    1.83 +    |> opt_block
    1.84      |> put_goal (Some (((kind atts, (PureThy.default_name name), prop), ([], goal)), after_qed))
    1.85      |> auto_bind_goal prop
    1.86      |> (if is_chain state then use_facts else reset_facts)