--- a/Nominal/Ex/LF.thy	Wed Mar 14 15:41:54 2012 +0000
+++ b/Nominal/Ex/LF.thy	Sat Mar 17 05:13:59 2012 +0000
@@ -147,14 +147,6 @@
 | tex: "\<lbrakk>\<Sigma>,\<Gamma> \<turnstile> A : \<Pi>[x:C].K; \<Sigma>,\<Gamma> \<turnstile> B : \<Pi>[x:C].K; \<Sigma>,\<Gamma> \<turnstile> C : Type; 
          \<Sigma>,(x,C)#\<Gamma> \<turnstile> TApp A (Var x) = TApp B (Var x) : K; atom x\<sharp>\<Gamma>\<rbrakk> \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> A = B : \<Pi>[x:C].K"
 
-thm sig_valid_ctx_valid_trm_valid_ty_valid_kind_valid_trm_equiv_ty_equiv_kind_equiv_def
-thm sig_valid_def
-thm trm_valid_def
-thm ty_valid_def
-thm kind_valid_def
-thm trm_equiv_def
-thm kind_equiv_def
-thm ty_equiv_def
 
 end