src/HOL/Nominal/Nominal.thy

   {* tactic to delete one inner occurence of fresh_fun *}
 
 
 (************************************************)
 (* main file for constructing nominal datatypes *)
+lemma allE_Nil: assumes "\<forall>x. P x" obtains "P []"
+  using assms ..
+
 use "nominal_package.ML"
 
 (******************************************************)
 (* primitive recursive functions on nominal datatypes *)
 use "nominal_primrec.ML"