Nominal/Ex/SingleLet.thy
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