Mercurialisabelle / diff
summary | shortlog | changelog | graph | tags | branches | files | changeset | file | revisions | annotate | diff | raw
src/Pure/tactic.ML
changeset 5838 a4122945d638
parent 5263 8862ed2db431
child 5956 ab4d13e9e77a 
     1.1 --- a/src/Pure/tactic.ML	Mon Nov 09 15:40:05 1998 +0100
     1.2 +++ b/src/Pure/tactic.ML	Mon Nov 09 15:40:26 1998 +0100
     1.3 @@ -60,7 +60,8 @@
     1.4    val make_elim		: thm -> thm
     1.5    val match_from_net_tac	: (int*thm) Net.net -> int -> tactic
     1.6    val match_tac	: thm list -> int -> tactic
     1.7 -  val metacut_tac	: thm -> int -> tactic   
     1.8 +  val metacut_tac	: thm -> int -> tactic
     1.9 +  val metacuts_tac	: thm list -> int -> tactic   
    1.10    val net_bimatch_tac	: (bool*thm) list -> int -> tactic
    1.11    val net_biresolve_tac	: (bool*thm) list -> int -> tactic
    1.12    val net_match_tac	: thm list -> int -> tactic
    1.13 @@ -321,6 +322,7 @@
    1.14  (*The conclusion of the rule gets assumed in subgoal i,
    1.15    while subgoal i+1,... are the premises of the rule.*)
    1.16  fun metacut_tac rule = bires_cut_tac [(false,rule)];
    1.17 +fun metacuts_tac rules i = EVERY (map (fn th => metacut_tac th i) rules);
    1.18  
    1.19  (*Recognizes theorems that are not rules, but simple propositions*)
    1.20  fun is_fact rl =
isabelle