--- a/Nominal/Ex/LetRec2.thy	Fri Nov 12 01:20:53 2010 +0000
+++ b/Nominal/Ex/LetRec2.thy	Sat Nov 13 10:25:03 2010 +0000
@@ -4,7 +4,6 @@
 
 atom_decl name
 
-
 nominal_datatype trm =
   Vr "name"
 | Ap "trm" "trm"
@@ -28,6 +27,10 @@
 thm trm_lts.distinct
 
 
+
+section {* Tests *}
+
+
 (* why is this not in HOL simpset? *)
 (*
 lemma set_sub: "{a, b} - {b} = {a} - {b}"