--- a/Nominal/Ex/Lambda.thy	Tue Dec 28 00:20:50 2010 +0000
+++ b/Nominal/Ex/Lambda.thy	Tue Dec 28 19:51:25 2010 +0000
@@ -20,33 +20,12 @@
 thm lam.size_eqvt
 
 
-section {* Strong Induction Lemma via Induct_schema *}
-
-
-lemma strong_induct:
-  fixes c::"'a::fs"
-  assumes a1: "\<And>name c. P c (Var name)"
-  and     a2: "\<And>lam1 lam2 c. \<lbrakk>\<And>d. P d lam1; \<And>d. P d lam2\<rbrakk> \<Longrightarrow> P c (App lam1 lam2)"
-  and     a3: "\<And>name lam c. \<lbrakk>{atom name} \<sharp>* c; \<And>d. P d lam\<rbrakk> \<Longrightarrow> P c (Lam name lam)"
-  shows "P c lam"
-using assms
-apply(induction_schema)
-apply(rule_tac y="lam" in lam.strong_exhaust)
-apply(blast)
-apply(blast)
-apply(blast)
-apply(relation "measure (\<lambda>(x,y). size y)")
-apply(simp_all add: lam.size)
-done
-
 section {* Typing *}
 
 nominal_datatype ty =
   TVar string
-| TFun ty ty
+| TFun ty ty ("_ \<rightarrow> _") 
 
-notation
- TFun ("_ \<rightarrow> _") 
 
 (*
 declare ty.perm[eqvt]