# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1437387719 -3600
# Node ID 4af8a92396cedbe4dd46cc5f8e6d9849e7e58c33
# Parent  f80fa0d18d8107e79cbb3e8967d29908661d380e
removed junk

diff -r f80fa0d18d81 -r 4af8a92396ce Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Thu Jul 09 09:12:44 2015 +0100
+++ b/Nominal/Ex/Lambda.thy	Mon Jul 20 11:21:59 2015 +0100
@@ -14,14 +14,6 @@
 
 thm obtain_atom
 
-lemma 
- "(\<forall>thesis. (finite X \<longrightarrow> (\<forall>a. ((a \<notin> X \<and> sort_of a = s) \<longrightarrow> thesis)) \<longrightarrow> thesis)) \<longleftrightarrow>
-  (finite X \<longrightarrow> (\<exists> a. (a \<notin> X \<and> sort_of a = s)))"
-apply(auto) 
-done
-
-
-
 ML {* trace := true *}
 
 nominal_datatype lam =
@@ -996,8 +988,6 @@
 
 text {* tests of functions containing if and case *}
 
-consts P :: "lam \<Rightarrow> bool"
-
 (*
 nominal_function  
   A :: "lam => lam"