--- a/Nominal/Ex/Lambda.thy	Mon Apr 11 02:25:25 2011 +0100
+++ b/Nominal/Ex/Lambda.thy	Wed Apr 13 13:41:52 2011 +0100
@@ -2,6 +2,7 @@
 imports "../Nominal2" 
 begin
 
+
 atom_decl name
 
 nominal_datatype lam =
@@ -9,6 +10,17 @@
 | App "lam" "lam"
 | Lam x::"name" l::"lam"  bind x in l ("Lam [_]. _" [100, 100] 100)
 
+inductive 
+  triv :: "lam \<Rightarrow> nat \<Rightarrow> bool"
+where
+  Var: "triv (Var x) n"
+
+equivariance triv
+nominal_inductive triv avoids Var : "{}::name set"
+apply(auto simp add: fresh_star_def)
+done 
+
+
 text {* height function *}
 
 nominal_primrec
@@ -494,7 +506,6 @@
 
 
 
-
 end