# HG changeset patch
# User narboux
# Date 1177416083 -7200
# Node ID 8c64803fae4874d128433a4296d9af05acd93f5b
# Parent  9bb135fa520611763546f8a371dad42350790c97
adds op in front of an infix to fix SML compilation

diff -r 9bb135fa5206 -r 8c64803fae48 src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Mon Apr 23 20:44:12 2007 +0200
+++ b/src/HOL/Nominal/Nominal.thy	Tue Apr 24 14:01:23 2007 +0200
@@ -634,6 +634,11 @@
   shows "pi1 \<triangleq> pi2 \<Longrightarrow> (rev pi1) \<triangleq> (rev pi2)"
   by (simp add: at_prm_rev_eq[OF at])
 
+lemma at_perm_fresh_fresh:
+  fixes a  :: "'x"
+  assumes 
+
+
 lemma at_ds1:
   fixes a  :: "'x"
   assumes at: "at TYPE('x)"
diff -r 9bb135fa5206 -r 8c64803fae48 src/HOL/Nominal/nominal_fresh_fun.ML
--- a/src/HOL/Nominal/nominal_fresh_fun.ML	Mon Apr 23 20:44:12 2007 +0200
+++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Tue Apr 24 14:01:23 2007 +0200
@@ -9,11 +9,13 @@
 (* First some functions that could be
  in the library *)
 
-(* A tactical which implements Coq's T;[a,b,c] *)
+(* A tactical which applies a list of int -> tactic to the corresponding subgoals present after the application of another tactic. 
+T THENL [A,B,C] is equivalent to T THEN (C 3 THEN B 2 THEN A 1) 
+*)
 
 infix 1 THENL
 
-fun THENL (tac,tacs) =
+fun (op THENL) (tac,tacs) =
  tac THEN
   (EVERY (map  (fn (tac,i) => tac i) (rev tacs ~~ (length tacs downto 1))))