Nominal/Ex/Let.thy
changeset 2926 37c0d7953cba
parent 2925 b4404b13f775
child 2931 aaef9dec5e1d
--- a/Nominal/Ex/Let.thy	Wed Jun 29 17:01:09 2011 +0100
+++ b/Nominal/Ex/Let.thy	Wed Jun 29 19:21:26 2011 +0100
@@ -2,6 +2,7 @@
 imports "../Nominal2" 
 begin
 
+
 atom_decl name
 
 nominal_datatype trm =
@@ -305,6 +306,7 @@
   apply (erule alpha_bn_inducts)
  oops
 
+
 end