summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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