changeset 2107 | 5686d83db1f9 |
parent 2106 | 409ecb7284dd |
child 2118 | 0e52851acac4 |
--- a/Nominal/Ex/SingleLet.thy Wed May 12 13:43:48 2010 +0100 +++ b/Nominal/Ex/SingleLet.thy Wed May 12 14:47:52 2010 +0100 @@ -16,7 +16,7 @@ where "bn (As x t) = {atom x}" - +ML {* Inductive.the_inductive *} thm trm_assg.fv thm trm_assg.supp thm trm_assg.eq_iff @@ -31,6 +31,7 @@ equivariance alpha_trm_raw + end