--- a/Nominal/Ex/Lambda.thy	Thu Aug 19 18:24:36 2010 +0800
+++ b/Nominal/Ex/Lambda.thy	Sat Aug 21 16:20:10 2010 +0800
@@ -1,15 +1,18 @@
 theory Lambda
-imports "../NewParser" Quotient_Option
+imports "../NewParser" 
 begin
 
 atom_decl name
-declare [[STEPS = 9]]
+declare [[STEPS = 20]]
 
-nominal_datatype lam =
+nominal_datatype  lam =
   Var "name"
 | App "lam" "lam"
 | Lam x::"name" l::"lam"  bind x in l
 
+
+thm eq_iff
+
 thm lam.fv
 thm lam.supp
 lemmas supp_fn' = lam.fv[simplified lam.supp]