src/HOL/Nominal/nominal_fresh_fun.ML
changeset 22774 8c64803fae48
parent 22753 49d7818e6161
child 22787 85e7e32e6004
     1.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML	Mon Apr 23 20:44:12 2007 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Tue Apr 24 14:01:23 2007 +0200
     1.3 @@ -9,11 +9,13 @@
     1.4  (* First some functions that could be
     1.5   in the library *)
     1.6  
     1.7 -(* A tactical which implements Coq's T;[a,b,c] *)
     1.8 +(* A tactical which applies a list of int -> tactic to the corresponding subgoals present after the application of another tactic. 
     1.9 +T THENL [A,B,C] is equivalent to T THEN (C 3 THEN B 2 THEN A 1) 
    1.10 +*)
    1.11  
    1.12  infix 1 THENL
    1.13  
    1.14 -fun THENL (tac,tacs) =
    1.15 +fun (op THENL) (tac,tacs) =
    1.16   tac THEN
    1.17    (EVERY (map  (fn (tac,i) => tac i) (rev tacs ~~ (length tacs downto 1))))
    1.18