| changeset 27228 | 4f7976a6ffc3 |
| parent 26847 | 9254cca608ef |
| child 27374 | 2a3c22fd95ab |
--- a/src/HOL/Nominal/Nominal.thy Mon Jun 16 17:54:38 2008 +0200 +++ b/src/HOL/Nominal/Nominal.thy Mon Jun 16 17:54:39 2008 +0200 @@ -3528,6 +3528,9 @@ (************************************************) (* main file for constructing nominal datatypes *) +lemma allE_Nil: assumes "\<forall>x. P x" obtains "P []" + using assms .. + use "nominal_package.ML" (******************************************************)