Pure/tactic/subgoals_tac: new (moved from ZF/Order.ML)
authorlcp
Fri Jun 24 10:45:02 1994 +0200 (1994-06-24)
changeset 439ad3f46c13f1e
parent 438 52e8393ccd77
child 440 1577cbcd0936
Pure/tactic/subgoals_tac: new (moved from ZF/Order.ML)
src/Pure/tactic.ML
     1.1 --- a/src/Pure/tactic.ML	Thu Jun 23 17:52:58 1994 +0200
     1.2 +++ b/src/Pure/tactic.ML	Fri Jun 24 10:45:02 1994 +0200
     1.3 @@ -66,8 +66,9 @@
     1.4    val rewtac: thm -> tactic
     1.5    val rtac: thm -> int -> tactic
     1.6    val rule_by_tactic: tactic -> thm -> thm
     1.7 +  val subgoal_tac: string -> int -> tactic
     1.8 +  val subgoals_tac: string list -> int -> tactic
     1.9    val subgoals_of_brl: bool * thm -> int
    1.10 -  val subgoal_tac: string -> int -> tactic
    1.11    val trace_goalno_tac: (int -> tactic) -> int -> tactic
    1.12    end
    1.13  end;
    1.14 @@ -261,6 +262,9 @@
    1.15  (*Introduce the given proposition as a lemma and subgoal*)
    1.16  fun subgoal_tac sprop = res_inst_tac [("psi", sprop)] cut_rl;
    1.17  
    1.18 +(*Introduce a list of lemmas and subgoals*)
    1.19 +fun subgoals_tac sprops = EVERY' (map subgoal_tac sprops);
    1.20 +
    1.21  
    1.22  (**** Indexing and filtering of theorems ****)
    1.23