# HG changeset patch
# User urbanc
# Date 1176385572 -7200
# Node ID 0c5b22076fb3707e49150223d6a9d73acc9164cc
# Parent  6cf96b9f7b9e7f6b2afebd3aca5630fc19a900ab
tuned the proof of lemma pt_list_set_fresh (as suggested by Randy Pollack) and tuned the syntax for sub_contexts

diff -r 6cf96b9f7b9e -r 0c5b22076fb3 src/HOL/Nominal/Examples/Crary.thy
--- a/src/HOL/Nominal/Examples/Crary.thy	Thu Apr 12 15:35:29 2007 +0200
+++ b/src/HOL/Nominal/Examples/Crary.thy	Thu Apr 12 15:46:12 2007 +0200
@@ -267,14 +267,14 @@
   valid_cons_elim_auto[elim]:"valid ((x,T)#\<Gamma>)"
 
 abbreviation
-  "sub_context" :: "Ctxt \<Rightarrow> Ctxt \<Rightarrow> bool" (" _ \<lless> _ " [55,55] 55)
+  "sub_context" :: "Ctxt \<Rightarrow> Ctxt \<Rightarrow> bool" (" _ \<subseteq> _ " [55,55] 55)
 where
-  "\<Gamma>\<^isub>1 \<lless> \<Gamma>\<^isub>2 \<equiv> \<forall>a T. (a,T)\<in>set \<Gamma>\<^isub>1 \<longrightarrow> (a,T)\<in>set \<Gamma>\<^isub>2"
+  "\<Gamma>\<^isub>1 \<subseteq> \<Gamma>\<^isub>2 \<equiv> \<forall>a T. (a,T)\<in>set \<Gamma>\<^isub>1 \<longrightarrow> (a,T)\<in>set \<Gamma>\<^isub>2"
 
 lemma valid_monotonicity[elim]:
- assumes a: "\<Gamma> \<lless> \<Gamma>'" 
+ assumes a: "\<Gamma> \<subseteq> \<Gamma>'" 
  and     b: "x\<sharp>\<Gamma>'"
- shows "(x,T\<^isub>1)#\<Gamma> \<lless> (x,T\<^isub>1)#\<Gamma>'"
+ shows "(x,T\<^isub>1)#\<Gamma> \<subseteq> (x,T\<^isub>1)#\<Gamma>'"
 using a b by auto
 
 lemma fresh_context: 
@@ -298,8 +298,8 @@
 inductive2
   typing :: "Ctxt\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" (" _ \<turnstile> _ : _ " [60,60,60] 60) 
 where
-  t_Var[intro]:   "\<lbrakk>valid \<Gamma>; (x,T)\<in>set \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> Var x : T"
-| t_App[intro]:   "\<lbrakk>\<Gamma> \<turnstile> e\<^isub>1 : T\<^isub>1\<rightarrow>T\<^isub>2; \<Gamma> \<turnstile> e\<^isub>2 : T\<^isub>1\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> App e\<^isub>1 e\<^isub>2 : T\<^isub>2"
+  t_Var[intro]:   "\<lbrakk>valid \<Gamma>; (x,T)\<in>set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x : T"
+| t_App[intro]:   "\<lbrakk>\<Gamma> \<turnstile> e\<^isub>1 : T\<^isub>1\<rightarrow>T\<^isub>2; \<Gamma> \<turnstile> e\<^isub>2 : T\<^isub>1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App e\<^isub>1 e\<^isub>2 : T\<^isub>2"
 | t_Lam[intro]:   "\<lbrakk>x\<sharp>\<Gamma>; (x,T\<^isub>1)#\<Gamma> \<turnstile> t : T\<^isub>2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [x].t : T\<^isub>1\<rightarrow>T\<^isub>2"
 | t_Const[intro]: "valid \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> Const n : TBase"
 | t_Unit[intro]:  "valid \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> Unit : TUnit"
@@ -440,16 +440,16 @@
 section {* Algorithmic Term Equivalence and Algorithmic Path Equivalence *}
 
 inductive2
-  alg_equiv :: "Ctxt\<Rightarrow>trm\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" ("_ \<turnstile> _ \<Leftrightarrow> _ : _" [60,60] 60) 
+  alg_equiv :: "Ctxt\<Rightarrow>trm\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" ("_ \<turnstile> _ \<Leftrightarrow> _ : _" [60,60,60,60] 60) 
 and
-  alg_path_equiv :: "Ctxt\<Rightarrow>trm\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" ("_ \<turnstile> _ \<leftrightarrow> _ : _" [60,60] 60) 
+  alg_path_equiv :: "Ctxt\<Rightarrow>trm\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" ("_ \<turnstile> _ \<leftrightarrow> _ : _" [60,60,60,60] 60) 
 where
-  QAT_Base[intro]:  "\<lbrakk>s \<Down> p; t \<Down> q; \<Gamma> \<turnstile> p \<leftrightarrow> q : TBase \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s \<Leftrightarrow> t : TBase"
+  QAT_Base[intro]:  "\<lbrakk>s \<Down> p; t \<Down> q; \<Gamma> \<turnstile> p \<leftrightarrow> q : TBase\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s \<Leftrightarrow> t : TBase"
 | QAT_Arrow[intro]: "\<lbrakk>x\<sharp>(\<Gamma>,s,t); (x,T\<^isub>1)#\<Gamma> \<turnstile> App s (Var x) \<Leftrightarrow> App t (Var x) : T\<^isub>2\<rbrakk> 
                      \<Longrightarrow> \<Gamma> \<turnstile> s \<Leftrightarrow> t : T\<^isub>1 \<rightarrow> T\<^isub>2"
 | QAT_One[intro]:   "valid \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> s \<Leftrightarrow> t : TUnit"
 | QAP_Var[intro]:   "\<lbrakk>valid \<Gamma>;(x,T) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x \<leftrightarrow> Var x : T"
-| QAP_App[intro]:   "\<lbrakk>\<Gamma> \<turnstile> p \<leftrightarrow> q : T\<^isub>1 \<rightarrow> T\<^isub>2; \<Gamma> \<turnstile> s \<Leftrightarrow> t : T\<^isub>1 \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App p s \<leftrightarrow> App q t : T\<^isub>2"
+| QAP_App[intro]:   "\<lbrakk>\<Gamma> \<turnstile> p \<leftrightarrow> q : T\<^isub>1 \<rightarrow> T\<^isub>2; \<Gamma> \<turnstile> s \<Leftrightarrow> t : T\<^isub>1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App p s \<leftrightarrow> App q t : T\<^isub>2"
 | QAP_Const[intro]: "valid \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> Const n \<leftrightarrow> Const n : TBase"
 
 nominal_inductive alg_equiv
@@ -579,17 +579,17 @@
 done
 
 lemma algorithmic_monotonicity:
-  shows "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T \<Longrightarrow> \<Gamma> \<lless> \<Gamma>' \<Longrightarrow> valid \<Gamma>' \<Longrightarrow> \<Gamma>' \<turnstile> s \<Leftrightarrow> t : T"
-  and   "\<Gamma> \<turnstile> s \<leftrightarrow> t : T \<Longrightarrow> \<Gamma> \<lless> \<Gamma>' \<Longrightarrow> valid \<Gamma>' \<Longrightarrow> \<Gamma>' \<turnstile> s \<leftrightarrow> t : T"
+  shows "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T \<Longrightarrow> \<Gamma> \<subseteq> \<Gamma>' \<Longrightarrow> valid \<Gamma>' \<Longrightarrow> \<Gamma>' \<turnstile> s \<Leftrightarrow> t : T"
+  and   "\<Gamma> \<turnstile> s \<leftrightarrow> t : T \<Longrightarrow> \<Gamma> \<subseteq> \<Gamma>' \<Longrightarrow> valid \<Gamma>' \<Longrightarrow> \<Gamma>' \<turnstile> s \<leftrightarrow> t : T"
 proof (nominal_induct \<Gamma> s t T and \<Gamma> s t T avoiding: \<Gamma>' rule: alg_equiv_alg_path_equiv.strong_inducts)
  case (QAT_Arrow x \<Gamma> s t T\<^isub>1 T\<^isub>2 \<Gamma>')
   have fs:"x\<sharp>\<Gamma>" "x\<sharp>s" "x\<sharp>t" "x\<sharp>\<Gamma>'"by fact
-  have h2:"\<Gamma>\<lless>\<Gamma>'" by fact
-  have ih:"\<And>\<Gamma>'. \<lbrakk>(x,T\<^isub>1)#\<Gamma> \<lless> \<Gamma>'; valid \<Gamma>'\<rbrakk>  \<Longrightarrow> \<Gamma>' \<turnstile> App s (Var x) \<Leftrightarrow> App t (Var x) : T\<^isub>2" by fact
+  have h2:"\<Gamma> \<subseteq> \<Gamma>'" by fact
+  have ih:"\<And>\<Gamma>'. \<lbrakk>(x,T\<^isub>1)#\<Gamma> \<subseteq> \<Gamma>'; valid \<Gamma>'\<rbrakk>  \<Longrightarrow> \<Gamma>' \<turnstile> App s (Var x) \<Leftrightarrow> App t (Var x) : T\<^isub>2" by fact
   have "valid \<Gamma>'" by fact
   then have "valid ((x,T\<^isub>1)#\<Gamma>')" using fs by auto
   moreover
-  have sub: "(x,T\<^isub>1)#\<Gamma> \<lless> (x,T\<^isub>1)#\<Gamma>'" using h2 by auto
+  have sub: "(x,T\<^isub>1)#\<Gamma> \<subseteq> (x,T\<^isub>1)#\<Gamma>'" using h2 by auto
   ultimately have "(x,T\<^isub>1)#\<Gamma>' \<turnstile> App s (Var x) \<Leftrightarrow> App t (Var x) : T\<^isub>2" using ih by simp
   then show "\<Gamma>' \<turnstile> s \<Leftrightarrow> t : T\<^isub>1\<rightarrow>T\<^isub>2" using fs by (auto simp add: fresh_prod)
 qed (auto)
@@ -607,7 +607,7 @@
    "\<Gamma> \<turnstile> s is t : TUnit = True"
  | "\<Gamma> \<turnstile> s is t : TBase = \<Gamma> \<turnstile> s \<Leftrightarrow> t : TBase"
  | "\<Gamma> \<turnstile> s is t : (T\<^isub>1 \<rightarrow> T\<^isub>2) =  
-    (\<forall>\<Gamma>' s' t'. \<Gamma>\<lless>\<Gamma>' \<longrightarrow> valid \<Gamma>' \<longrightarrow> \<Gamma>' \<turnstile> s' is t' : T\<^isub>1 \<longrightarrow>  (\<Gamma>' \<turnstile> (App s s') is (App t t') : T\<^isub>2))"
+    (\<forall>\<Gamma>' s' t'. \<Gamma>\<subseteq>\<Gamma>' \<longrightarrow> valid \<Gamma>' \<longrightarrow> \<Gamma>' \<turnstile> s' is t' : T\<^isub>1 \<longrightarrow>  (\<Gamma>' \<turnstile> (App s s') is (App t t') : T\<^isub>2))"
 apply (auto simp add: ty.inject)
 apply (subgoal_tac "(\<exists>T\<^isub>1 T\<^isub>2. b=T\<^isub>1 \<rightarrow> T\<^isub>2) \<or> b=TUnit \<or> b=TBase" )
 apply (force)
@@ -621,7 +621,7 @@
 
 lemma logical_monotonicity :
  assumes a1: "\<Gamma> \<turnstile> s is t : T" 
- and     a2: "\<Gamma>\<lless>\<Gamma>'" 
+ and     a2: "\<Gamma> \<subseteq> \<Gamma>'" 
  and     a3: "valid \<Gamma>'"
  shows "\<Gamma>' \<turnstile> s is t : T"
 using a1 a2 a3
@@ -631,7 +631,7 @@
 next
   case (3 \<Gamma> s t T\<^isub>1 T\<^isub>2 \<Gamma>')
   have "\<Gamma> \<turnstile> s is t : T\<^isub>1\<rightarrow>T\<^isub>2" 
-  and  "\<Gamma> \<lless> \<Gamma>'" 
+  and  "\<Gamma> \<subseteq> \<Gamma>'" 
   and  "valid \<Gamma>'" by fact
   then show "\<Gamma>' \<turnstile> s is t : T\<^isub>1\<rightarrow>T\<^isub>2" by simp
 qed (auto)
@@ -661,7 +661,7 @@
     have ih2:"\<And>\<Gamma> s t. \<lbrakk>\<Gamma> \<turnstile> s is t : T\<^isub>1; valid \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s \<Leftrightarrow> t : T\<^isub>1" by fact
     {
       fix \<Gamma>' s t
-      assume "\<Gamma>\<lless>\<Gamma>'" and hl:"\<Gamma>' \<turnstile> s is t : T\<^isub>1" and hk: "valid \<Gamma>'"
+      assume "\<Gamma> \<subseteq> \<Gamma>'" and hl:"\<Gamma>' \<turnstile> s is t : T\<^isub>1" and hk: "valid \<Gamma>'"
       then have "\<Gamma>' \<turnstile> p \<leftrightarrow> q : T\<^isub>1 \<rightarrow> T\<^isub>2" using h algorithmic_monotonicity by auto
       moreover have "\<Gamma>' \<turnstile> s \<Leftrightarrow> t : T\<^isub>1" using ih2 hl hk by auto
       ultimately have "\<Gamma>' \<turnstile> App p s \<leftrightarrow> App q t : T\<^isub>2" by auto
@@ -707,7 +707,7 @@
   have ih2:"\<And>\<Gamma> s t u. \<lbrakk>\<Gamma> \<turnstile> s is t : T\<^isub>2; \<Gamma> \<turnstile> t is u : T\<^isub>2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s is u : T\<^isub>2" by fact
   {
     fix \<Gamma>' s' u'
-    assume hsub:"\<Gamma>\<lless>\<Gamma>'" and hl:"\<Gamma>' \<turnstile> s' is u' : T\<^isub>1" and hk: "valid \<Gamma>'"
+    assume hsub:"\<Gamma> \<subseteq> \<Gamma>'" and hl:"\<Gamma>' \<turnstile> s' is u' : T\<^isub>1" and hk: "valid \<Gamma>'"
     then have "\<Gamma>' \<turnstile> u' is s' : T\<^isub>1" using logical_symmetry by blast
     then have "\<Gamma>' \<turnstile> u' is u' : T\<^isub>1" using ih1 hl by blast
     then have "\<Gamma>' \<turnstile> App t u' is App u u' : T\<^isub>2" using h2 hsub hk by auto
@@ -742,11 +742,11 @@
   have ih:"\<And>\<Gamma> s t s'. \<lbrakk>\<Gamma> \<turnstile> s is t : T\<^isub>2; s' \<leadsto> s\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s' is t : T\<^isub>2" by fact
   have h2:"\<Gamma> \<turnstile> s is t : T\<^isub>1\<rightarrow>T\<^isub>2" by fact
   then 
-  have hb:"\<forall>\<Gamma>' s' t'. \<Gamma>\<lless>\<Gamma>' \<longrightarrow> valid \<Gamma>' \<longrightarrow> \<Gamma>' \<turnstile> s' is t' : T\<^isub>1 \<longrightarrow> (\<Gamma>' \<turnstile> (App s s') is (App t t') : T\<^isub>2)" 
+  have hb:"\<forall>\<Gamma>' s' t'. \<Gamma>\<subseteq>\<Gamma>' \<longrightarrow> valid \<Gamma>' \<longrightarrow> \<Gamma>' \<turnstile> s' is t' : T\<^isub>1 \<longrightarrow> (\<Gamma>' \<turnstile> (App s s') is (App t t') : T\<^isub>2)" 
     by auto
   {
     fix \<Gamma>' s\<^isub>2 t\<^isub>2
-    assume "\<Gamma>\<lless>\<Gamma>'" and "\<Gamma>' \<turnstile> s\<^isub>2 is t\<^isub>2 : T\<^isub>1" and "valid \<Gamma>'"
+    assume "\<Gamma> \<subseteq> \<Gamma>'" and "\<Gamma>' \<turnstile> s\<^isub>2 is t\<^isub>2 : T\<^isub>1" and "valid \<Gamma>'"
     then have "\<Gamma>' \<turnstile> (App s s\<^isub>2) is (App t t\<^isub>2) : T\<^isub>2" using hb by auto
     moreover have "(App s' s\<^isub>2)  \<leadsto> (App s s\<^isub>2)" using h1 by auto  
     ultimately have "\<Gamma>' \<turnstile> App s' s\<^isub>2 is App t t\<^isub>2 : T\<^isub>2" using ih by auto
@@ -770,7 +770,7 @@
 
 lemma logical_subst_monotonicity :
   assumes a: "\<Gamma>' \<turnstile> s is t over \<Gamma>" 
-  and     b: "\<Gamma>'\<lless>\<Gamma>''"
+  and     b: "\<Gamma>' \<subseteq> \<Gamma>''"
   and     c: "valid \<Gamma>''"
   shows "\<Gamma>'' \<turnstile> s is t over \<Gamma>"
 using a b c logical_monotonicity by blast
@@ -817,7 +817,7 @@
   have ih:"\<And> \<Gamma>' \<theta> \<theta>'. \<lbrakk>\<Gamma>' \<turnstile> \<theta> is \<theta>' over (x,T\<^isub>1)#\<Gamma>; valid \<Gamma>'\<rbrakk> \<Longrightarrow> \<Gamma>' \<turnstile> \<theta><t\<^isub>2> is \<theta>'<t\<^isub>2> : T\<^isub>2" by fact
   {
     fix \<Gamma>'' s' t'
-    assume "\<Gamma>'\<lless>\<Gamma>''" and hl:"\<Gamma>''\<turnstile> s' is t' : T\<^isub>1" and v: "valid \<Gamma>''"
+    assume "\<Gamma>' \<subseteq> \<Gamma>''" and hl:"\<Gamma>''\<turnstile> s' is t' : T\<^isub>1" and v: "valid \<Gamma>''"
     then have "\<Gamma>'' \<turnstile> \<theta> is \<theta>' over \<Gamma>" using logical_subst_monotonicity h by blast
     then have "\<Gamma>'' \<turnstile> (x,s')#\<theta> is (x,t')#\<theta>' over (x,T\<^isub>1)#\<Gamma>" using equiv_subst_ext hl fs by blast
     then have "\<Gamma>'' \<turnstile> (x,s')#\<theta><t\<^isub>2> is (x,t')#\<theta>'<t\<^isub>2> : T\<^isub>2" using ih v by auto
@@ -869,7 +869,7 @@
   have ih:"\<And>\<Gamma>' \<theta> \<theta>'. \<lbrakk>\<Gamma>' \<turnstile> \<theta> is \<theta>' over (x,T\<^isub>1)#\<Gamma>; valid \<Gamma>'\<rbrakk> \<Longrightarrow> \<Gamma>' \<turnstile> \<theta><s\<^isub>2> is \<theta>'<t\<^isub>2> : T\<^isub>2" by fact
   {
     fix \<Gamma>'' s' t'
-    assume "\<Gamma>'\<lless>\<Gamma>''" and hl:"\<Gamma>''\<turnstile> s' is t' : T\<^isub>1" and hk: "valid \<Gamma>''"
+    assume "\<Gamma>' \<subseteq> \<Gamma>''" and hl:"\<Gamma>''\<turnstile> s' is t' : T\<^isub>1" and hk: "valid \<Gamma>''"
     then have "\<Gamma>'' \<turnstile> \<theta> is \<theta>' over \<Gamma>" using h2 logical_subst_monotonicity by blast
     then have "\<Gamma>'' \<turnstile> (x,s')#\<theta> is (x,t')#\<theta>' over (x,T\<^isub>1)#\<Gamma>" using equiv_subst_ext hl fs by blast
     then have "\<Gamma>'' \<turnstile> (x,s')#\<theta><s\<^isub>2> is (x,t')#\<theta>'<t\<^isub>2> : T\<^isub>2" using ih hk by blast
@@ -911,7 +911,7 @@
                           \<Longrightarrow> \<Gamma>' \<turnstile> \<theta><App s (Var x)> is \<theta>'<App t (Var x)> : T\<^isub>2" by fact
    {
     fix \<Gamma>'' s' t'
-    assume hsub: "\<Gamma>'\<lless>\<Gamma>''" and hl: "\<Gamma>''\<turnstile> s' is t' : T\<^isub>1" and hk: "valid \<Gamma>''"
+    assume hsub: "\<Gamma>' \<subseteq> \<Gamma>''" and hl: "\<Gamma>''\<turnstile> s' is t' : T\<^isub>1" and hk: "valid \<Gamma>''"
     then have "\<Gamma>'' \<turnstile> \<theta> is \<theta>' over \<Gamma>" using h2 logical_subst_monotonicity by blast
     then have "\<Gamma>'' \<turnstile> (x,s')#\<theta> is (x,t')#\<theta>' over (x,T\<^isub>1)#\<Gamma>" using equiv_subst_ext hl fs by blast
     then have "\<Gamma>'' \<turnstile> (x,s')#\<theta><App s (Var x)>  is (x,t')#\<theta>'<App t (Var x)> : T\<^isub>2" using ih hk by blast
diff -r 6cf96b9f7b9e -r 0c5b22076fb3 src/HOL/Nominal/Examples/SN.thy
--- a/src/HOL/Nominal/Examples/SN.thy	Thu Apr 12 15:35:29 2007 +0200
+++ b/src/HOL/Nominal/Examples/SN.thy	Thu Apr 12 15:46:12 2007 +0200
@@ -160,29 +160,28 @@
 using a b c
 by (induct \<Gamma>) (auto dest!: fresh_context)
 
-inductive2 typing :: "(name\<times>ty) list\<Rightarrow>lam\<Rightarrow>ty\<Rightarrow>bool" (" _ \<turnstile> _ : _ " [80,80,80] 80)
+inductive2 typing :: "(name\<times>ty) list\<Rightarrow>lam\<Rightarrow>ty\<Rightarrow>bool" ("_ \<turnstile> _ : _" [60,60,60] 60)
 where
-  t1[intro]: "\<lbrakk>valid \<Gamma>; (a,\<tau>)\<in>set \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> Var a : \<tau>"
-| t2[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : \<tau>\<rightarrow>\<sigma>; \<Gamma> \<turnstile> t2 : \<tau>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : \<sigma>"
+  t1[intro]: "\<lbrakk>valid \<Gamma>; (a,\<tau>)\<in>set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var a : \<tau>"
+| t2[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : \<tau>\<rightarrow>\<sigma>; \<Gamma> \<turnstile> t2 : \<tau>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : \<sigma>"
 | t3[intro]: "\<lbrakk>a\<sharp>\<Gamma>;((a,\<tau>)#\<Gamma>) \<turnstile> t : \<sigma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [a].t : \<tau>\<rightarrow>\<sigma>"
 
 nominal_inductive typing
   by (simp_all add: abs_fresh fresh_ty)
 
 abbreviation
-  "sub" :: "(name\<times>ty) list \<Rightarrow> (name\<times>ty) list \<Rightarrow> bool" (" _ \<lless> _ " [80,80] 80) where
-  "\<Gamma>1 \<lless> \<Gamma>2 \<equiv> \<forall>a \<sigma>. (a,\<sigma>)\<in>set \<Gamma>1 \<longrightarrow>  (a,\<sigma>)\<in>set \<Gamma>2"
+  "sub" :: "(name\<times>ty) list \<Rightarrow> (name\<times>ty) list \<Rightarrow> bool" ("_ \<subseteq> _" [60,60] 60) 
+where
+  "\<Gamma>1 \<subseteq> \<Gamma>2 \<equiv> \<forall>a \<sigma>. (a,\<sigma>)\<in>set \<Gamma>1 \<longrightarrow>  (a,\<sigma>)\<in>set \<Gamma>2"
 
 lemma weakening: 
   assumes a: "\<Gamma>1 \<turnstile> t : \<sigma>" 
   and     b: "valid \<Gamma>2" 
-  and     c: "\<Gamma>1 \<lless> \<Gamma>2"
-  shows "\<Gamma>2 \<turnstile> t:\<sigma>"
+  and     c: "\<Gamma>1 \<subseteq> \<Gamma>2"
+  shows "\<Gamma>2 \<turnstile> t : \<sigma>"
 using a b c
 apply(nominal_induct \<Gamma>1 t \<sigma> avoiding: \<Gamma>2 rule: typing.strong_induct)
 apply(auto | atomize)+
-(* FIXME: before using meta-connectives and the new induction *)
-(* method, this was completely automatic *)
 done
 
 lemma in_ctxt: 
@@ -208,7 +207,7 @@
 apply(auto simp add: lam.inject lam.distinct)
 done
 
-lemma t3_elim: "\<lbrakk>\<Gamma> \<turnstile> Lam [a].t : \<sigma>;a\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> \<exists>\<tau> \<tau>'. \<sigma>=\<tau>\<rightarrow>\<tau>' \<and> ((a,\<tau>)#\<Gamma>) \<turnstile> t : \<tau>'"
+lemma t3_elim: "\<lbrakk>\<Gamma> \<turnstile> Lam [a].t : \<sigma>;a\<sharp>\<Gamma>\<rbrakk> \<Longrightarrow> \<exists>\<tau> \<tau>'. \<sigma>=\<tau>\<rightarrow>\<tau>' \<and> (a,\<tau>)#\<Gamma> \<turnstile> t : \<tau>'"
 apply(ind_cases2 "\<Gamma> \<turnstile> Lam [a].t : \<sigma>")
 apply(auto simp add: lam.distinct lam.inject alpha) 
 apply(drule_tac pi="[(a,aa)]::name prm" in typing.eqvt)
@@ -225,14 +224,14 @@
 using a by (induct, auto)
 
 lemma ty_subs:
-  assumes a: "((c,\<sigma>)#\<Gamma>) \<turnstile> t1:\<tau>"
+  assumes a: "(c,\<sigma>)#\<Gamma> \<turnstile> t1:\<tau>"
   and     b: "\<Gamma>\<turnstile> t2:\<sigma>"
   shows  "\<Gamma> \<turnstile> t1[c::=t2]:\<tau>"
 using a b
 proof(nominal_induct t1 avoiding: \<Gamma> \<sigma> \<tau> c t2 rule: lam.induct)
   case (Var a) 
   have a1: "\<Gamma> \<turnstile>t2:\<sigma>" by fact
-  have a2: "((c,\<sigma>)#\<Gamma>) \<turnstile> Var a:\<tau>" by fact
+  have a2: "(c,\<sigma>)#\<Gamma> \<turnstile> Var a : \<tau>" by fact
   hence a21: "(a,\<tau>)\<in>set((c,\<sigma>)#\<Gamma>)" and a22: "valid((c,\<sigma>)#\<Gamma>)" by (auto dest: t1_elim)
   from a22 have a23: "valid \<Gamma>" and a24: "c\<sharp>\<Gamma>" by (auto dest: valid_elim) 
   from a24 have a25: "\<not>(\<exists>\<tau>. (c,\<tau>)\<in>set \<Gamma>)" by (rule fresh_context)
@@ -260,7 +259,7 @@
   have ih_s1: "\<And>c \<sigma> \<tau> t2 \<Gamma>. ((c,\<sigma>)#\<Gamma>) \<turnstile> s1:\<tau> \<Longrightarrow> \<Gamma>\<turnstile> t2: \<sigma> \<Longrightarrow> \<Gamma> \<turnstile> s1[c::=t2]:\<tau>" by fact
   have ih_s2: "\<And>c \<sigma> \<tau> t2 \<Gamma>. ((c,\<sigma>)#\<Gamma>) \<turnstile> s2:\<tau> \<Longrightarrow> \<Gamma>\<turnstile> t2: \<sigma> \<Longrightarrow> \<Gamma> \<turnstile> s2[c::=t2]:\<tau>" by fact
   have "((c,\<sigma>)#\<Gamma>)\<turnstile>App s1 s2 : \<tau>" by fact
-  hence "\<exists>\<tau>'. ((c,\<sigma>)#\<Gamma>)\<turnstile>s1:\<tau>'\<rightarrow>\<tau> \<and> ((c,\<sigma>)#\<Gamma>)\<turnstile>s2:\<tau>'" by (rule t2_elim) 
+  hence "\<exists>\<tau>'. (c,\<sigma>)#\<Gamma> \<turnstile>s1:\<tau>'\<rightarrow>\<tau> \<and> (c,\<sigma>)#\<Gamma> \<turnstile> s2 : \<tau>'" by (rule t2_elim) 
   then obtain \<tau>' where "((c,\<sigma>)#\<Gamma>)\<turnstile>s1:\<tau>'\<rightarrow>\<tau>" and "((c,\<sigma>)#\<Gamma>)\<turnstile>s2:\<tau>'" by blast
   moreover
   have "\<Gamma> \<turnstile>t2:\<sigma>" by fact
@@ -270,23 +269,23 @@
   have "a\<sharp>\<Gamma>" "a\<sharp>\<sigma>" "a\<sharp>\<tau>" "a\<sharp>c" "a\<sharp>t2" by fact 
   hence f1: "a\<sharp>\<Gamma>" and f2: "a\<noteq>c" and f2': "c\<sharp>a" and f3: "a\<sharp>t2" and f4: "a\<sharp>((c,\<sigma>)#\<Gamma>)"
     by (auto simp add: fresh_atm fresh_prod fresh_list_cons)
-  have c1: "((c,\<sigma>)#\<Gamma>)\<turnstile>Lam [a].s : \<tau>" by fact
-  hence "\<exists>\<tau>1 \<tau>2. \<tau>=\<tau>1\<rightarrow>\<tau>2 \<and> ((a,\<tau>1)#(c,\<sigma>)#\<Gamma>) \<turnstile> s : \<tau>2" using f4 by (auto dest: t3_elim) 
+  have c1: "(c,\<sigma>)#\<Gamma> \<turnstile> Lam [a].s : \<tau>" by fact
+  hence "\<exists>\<tau>1 \<tau>2. \<tau>=\<tau>1\<rightarrow>\<tau>2 \<and> (a,\<tau>1)#(c,\<sigma>)#\<Gamma> \<turnstile> s : \<tau>2" using f4 by (auto dest: t3_elim) 
   then obtain \<tau>1 \<tau>2 where c11: "\<tau>=\<tau>1\<rightarrow>\<tau>2" and c12: "((a,\<tau>1)#(c,\<sigma>)#\<Gamma>) \<turnstile> s : \<tau>2" by force
   from c12 have "valid ((a,\<tau>1)#(c,\<sigma>)#\<Gamma>)" by (rule typing_valid)
   hence ca: "valid \<Gamma>" and cb: "a\<sharp>\<Gamma>" and cc: "c\<sharp>\<Gamma>" 
     by (auto simp add: fresh_list_cons) 
-  from c12 have c14: "((c,\<sigma>)#(a,\<tau>1)#\<Gamma>) \<turnstile> s : \<tau>2"
+  from c12 have c14: "(c,\<sigma>)#(a,\<tau>1)#\<Gamma> \<turnstile> s : \<tau>2"
   proof -
-    have c2: "((a,\<tau>1)#(c,\<sigma>)#\<Gamma>) \<lless> ((c,\<sigma>)#(a,\<tau>1)#\<Gamma>)" by force
+    have c2: "(a,\<tau>1)#(c,\<sigma>)#\<Gamma> \<subseteq> (c,\<sigma>)#(a,\<tau>1)#\<Gamma>" by force
     have c3: "valid ((c,\<sigma>)#(a,\<tau>1)#\<Gamma>)"
       by (rule v2, rule v2, auto simp add: fresh_list_cons fresh_prod ca cb cc f2' fresh_ty)
     from c12 c2 c3 show ?thesis by (force intro: weakening)
   qed
   assume c8: "\<Gamma> \<turnstile> t2 : \<sigma>"
-  have c81: "((a,\<tau>1)#\<Gamma>)\<turnstile>t2 :\<sigma>"
+  have c81: "(a,\<tau>1)#\<Gamma> \<turnstile> t2 :\<sigma>"
   proof -
-    have c82: "\<Gamma> \<lless> ((a,\<tau>1)#\<Gamma>)" by force
+    have c82: "\<Gamma> \<subseteq> (a,\<tau>1)#\<Gamma>" by force
     have c83: "valid ((a,\<tau>1)#\<Gamma>)" using f1 ca by force
     with c8 c82 c83 show ?thesis by (force intro: weakening)
   qed
diff -r 6cf96b9f7b9e -r 0c5b22076fb3 src/HOL/Nominal/Examples/SOS.thy
--- a/src/HOL/Nominal/Examples/SOS.thy	Thu Apr 12 15:35:29 2007 +0200
+++ b/src/HOL/Nominal/Examples/SOS.thy	Thu Apr 12 15:46:12 2007 +0200
@@ -219,9 +219,9 @@
   valid_cons_inv_auto[elim]:"valid ((x,T)#\<Gamma>)"
 
 abbreviation
-  "sub" :: "(name\<times>ty) list \<Rightarrow> (name\<times>ty) list \<Rightarrow> bool" ("_ \<lless> _" [55,55] 55)
+  "sub" :: "(name\<times>ty) list \<Rightarrow> (name\<times>ty) list \<Rightarrow> bool" ("_ \<subseteq> _" [55,55] 55)
 where
-  "\<Gamma>\<^isub>1 \<lless> \<Gamma>\<^isub>2 \<equiv> \<forall>x T. (x,T)\<in>set \<Gamma>\<^isub>1 \<longrightarrow> (x,T)\<in>set \<Gamma>\<^isub>2"
+  "\<Gamma>\<^isub>1 \<subseteq> \<Gamma>\<^isub>2 \<equiv> \<forall>x T. (x,T)\<in>set \<Gamma>\<^isub>1 \<longrightarrow> (x,T)\<in>set \<Gamma>\<^isub>2"
 
 lemma type_unicity_in_context:
   assumes asm1: "(x,t\<^isub>2) \<in> set ((x,t\<^isub>1)#\<Gamma>)" 
@@ -362,17 +362,17 @@
 qed
 
 lemma weakening: 
-  assumes "\<Gamma>\<^isub>1 \<turnstile> e: T" and "valid \<Gamma>\<^isub>2" and "\<Gamma>\<^isub>1 \<lless> \<Gamma>\<^isub>2"
+  assumes "\<Gamma>\<^isub>1 \<turnstile> e: T" and "valid \<Gamma>\<^isub>2" and "\<Gamma>\<^isub>1 \<subseteq> \<Gamma>\<^isub>2"
   shows "\<Gamma>\<^isub>2 \<turnstile> e: T"
   using assms
 proof(nominal_induct \<Gamma>\<^isub>1 e T avoiding: \<Gamma>\<^isub>2 rule: typing.strong_induct)
   case (t_Lam x \<Gamma>\<^isub>1 T\<^isub>1 t T\<^isub>2 \<Gamma>\<^isub>2)
-  have ih: "\<lbrakk>valid ((x,T\<^isub>1)#\<Gamma>\<^isub>2); (x,T\<^isub>1)#\<Gamma>\<^isub>1 \<lless> (x,T\<^isub>1)#\<Gamma>\<^isub>2\<rbrakk> \<Longrightarrow> (x,T\<^isub>1)#\<Gamma>\<^isub>2 \<turnstile> t : T\<^isub>2" by fact
+  have ih: "\<lbrakk>valid ((x,T\<^isub>1)#\<Gamma>\<^isub>2); (x,T\<^isub>1)#\<Gamma>\<^isub>1 \<subseteq> (x,T\<^isub>1)#\<Gamma>\<^isub>2\<rbrakk> \<Longrightarrow> (x,T\<^isub>1)#\<Gamma>\<^isub>2 \<turnstile> t : T\<^isub>2" by fact
   have H1: "valid \<Gamma>\<^isub>2" by fact
-  have H2: "\<Gamma>\<^isub>1 \<lless> \<Gamma>\<^isub>2" by fact
+  have H2: "\<Gamma>\<^isub>1 \<subseteq> \<Gamma>\<^isub>2" by fact
   have fs: "x\<sharp>\<Gamma>\<^isub>2" by fact
   then have "valid ((x,T\<^isub>1)#\<Gamma>\<^isub>2)" using H1 by auto
-  moreover have "(x,T\<^isub>1)#\<Gamma>\<^isub>1 \<lless> (x,T\<^isub>1)#\<Gamma>\<^isub>2" using H2 by auto
+  moreover have "(x,T\<^isub>1)#\<Gamma>\<^isub>1 \<subseteq> (x,T\<^isub>1)#\<Gamma>\<^isub>2" using H2 by auto
   ultimately have "(x,T\<^isub>1)#\<Gamma>\<^isub>2 \<turnstile> t : T\<^isub>2" using ih by simp 
   thus "\<Gamma>\<^isub>2 \<turnstile> Lam [x].t : T\<^isub>1\<rightarrow>T\<^isub>2" using fs by auto
 next
@@ -398,7 +398,7 @@
   then have "valid ((x\<^isub>2,T\<^isub>2)#(x\<^isub>1,T\<^isub>1)#\<Gamma>)"
     by (auto simp: fresh_list_cons fresh_atm)
   moreover 
-  have "(x\<^isub>1,T\<^isub>1)#(x\<^isub>2,T\<^isub>2)#\<Gamma> \<lless> (x\<^isub>2,T\<^isub>2)#(x\<^isub>1,T\<^isub>1)#\<Gamma>" by auto
+  have "(x\<^isub>1,T\<^isub>1)#(x\<^isub>2,T\<^isub>2)#\<Gamma> \<subseteq> (x\<^isub>2,T\<^isub>2)#(x\<^isub>1,T\<^isub>1)#\<Gamma>" by auto
   ultimately show "(x\<^isub>2,T\<^isub>2)#(x\<^isub>1,T\<^isub>1)#\<Gamma> \<turnstile> e : T" using a by (auto intro: weakening)
 qed
 
diff -r 6cf96b9f7b9e -r 0c5b22076fb3 src/HOL/Nominal/Examples/Weakening.thy
--- a/src/HOL/Nominal/Examples/Weakening.thy	Thu Apr 12 15:35:29 2007 +0200
+++ b/src/HOL/Nominal/Examples/Weakening.thy	Thu Apr 12 15:46:12 2007 +0200
@@ -37,10 +37,10 @@
 
 text{* typing judgements *}
 inductive2
-  typing :: "(name\<times>ty) list\<Rightarrow>lam\<Rightarrow>ty\<Rightarrow>bool" (" _ \<turnstile> _ : _ " [80,80,80] 80) 
+  typing :: "(name\<times>ty) list\<Rightarrow>lam\<Rightarrow>ty\<Rightarrow>bool" ("_ \<turnstile> _ : _" [60,60,60] 60) 
 where
-    t_Var[intro]: "\<lbrakk>valid \<Gamma>; (x,T)\<in>set \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> Var x : T"
-  | t_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : T1\<rightarrow>T2; \<Gamma> \<turnstile> t2 : T1\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : T2"
+    t_Var[intro]: "\<lbrakk>valid \<Gamma>; (x,T)\<in>set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x : T"
+  | t_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : T1\<rightarrow>T2; \<Gamma> \<turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : T2"
   | t_Lam[intro]: "\<lbrakk>x\<sharp>\<Gamma>;((x,T1)#\<Gamma>) \<turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [x].t : T1\<rightarrow>T2"
 
 (* automatically deriving the strong induction principle *)
@@ -50,16 +50,16 @@
 text {* definition of a subcontext *}
 
 abbreviation
-  "sub_context" :: "(name\<times>ty) list \<Rightarrow> (name\<times>ty) list \<Rightarrow> bool" (" _ \<lless> _ " [80,80] 80) 
+  "sub_context" :: "(name\<times>ty) list \<Rightarrow> (name\<times>ty) list \<Rightarrow> bool" ("_ \<subseteq> _" [60,60] 60) 
 where
-  "\<Gamma>1 \<lless> \<Gamma>2 \<equiv> \<forall>x T. (x,T)\<in>set \<Gamma>1 \<longrightarrow> (x,T)\<in>set \<Gamma>2"
+  "\<Gamma>1 \<subseteq> \<Gamma>2 \<equiv> \<forall>x T. (x,T)\<in>set \<Gamma>1 \<longrightarrow> (x,T)\<in>set \<Gamma>2"
 
 text {* Now it comes: The Weakening Lemma *}
 
 lemma weakening_version1: 
   assumes a: "\<Gamma>1 \<turnstile> t : T" 
   and     b: "valid \<Gamma>2" 
-  and     c: "\<Gamma>1 \<lless> \<Gamma>2"
+  and     c: "\<Gamma>1 \<subseteq> \<Gamma>2"
   shows "\<Gamma>2 \<turnstile> t : T"
 using a b c
 by (nominal_induct \<Gamma>1 t T avoiding: \<Gamma>2 rule: typing.strong_induct)
@@ -69,14 +69,14 @@
   fixes \<Gamma>1::"(name\<times>ty) list"
   and   t ::"lam"
   and   \<tau> ::"ty"
-  assumes a: "\<Gamma>1 \<turnstile> t:T"
+  assumes a: "\<Gamma>1 \<turnstile> t : T"
   and     b: "valid \<Gamma>2" 
-  and     c: "\<Gamma>1 \<lless> \<Gamma>2"
-  shows "\<Gamma>2 \<turnstile> t:T"
+  and     c: "\<Gamma>1 \<subseteq> \<Gamma>2"
+  shows "\<Gamma>2 \<turnstile> t : T"
 using a b c
 proof (nominal_induct \<Gamma>1 t T avoiding: \<Gamma>2 rule: typing.strong_induct)
   case (t_Var \<Gamma>1 x T)  (* variable case *)
-  have "\<Gamma>1 \<lless> \<Gamma>2" by fact 
+  have "\<Gamma>1 \<subseteq> \<Gamma>2" by fact 
   moreover  
   have "valid \<Gamma>2" by fact 
   moreover 
@@ -85,46 +85,47 @@
 next
   case (t_Lam x \<Gamma>1 T1 t T2) (* lambda case *)
   have vc: "x\<sharp>\<Gamma>2" by fact   (* variable convention *)
-  have ih: "\<And>\<Gamma>3. \<lbrakk>valid \<Gamma>3; ((x,T1)#\<Gamma>1) \<lless> \<Gamma>3\<rbrakk> \<Longrightarrow>  \<Gamma>3 \<turnstile> t:T2" by fact
-  have "\<Gamma>1 \<lless> \<Gamma>2" by fact
-  then have "((x,T1)#\<Gamma>1) \<lless> ((x,T1)#\<Gamma>2)" by simp
+  have ih: "\<lbrakk>valid ((x,T1)#\<Gamma>2); (x,T1)#\<Gamma>1 \<subseteq> (x,T1)#\<Gamma>2\<rbrakk> \<Longrightarrow>  (x,T1)#\<Gamma>2 \<turnstile> t:T2" by fact
+  have "\<Gamma>1 \<subseteq> \<Gamma>2" by fact
+  then have "(x,T1)#\<Gamma>1 \<subseteq> (x,T1)#\<Gamma>2" by simp
   moreover
   have "valid \<Gamma>2" by fact
   then have "valid ((x,T1)#\<Gamma>2)" using vc by (simp add: v2)
-  ultimately have "((x,T1)#\<Gamma>2) \<turnstile> t:T2" using ih by simp
-  with vc show "\<Gamma>2 \<turnstile> (Lam [x].t) : T1\<rightarrow>T2" by auto
+  ultimately have "(x,T1)#\<Gamma>2 \<turnstile> t : T2" using ih by simp
+  with vc show "\<Gamma>2 \<turnstile> Lam [x].t : T1\<rightarrow>T2" by auto
 qed (auto) (* app case *)
 
 lemma weakening_version3: 
   assumes a: "\<Gamma>1 \<turnstile> t : T"
   and     b: "valid \<Gamma>2" 
-  and     c: "\<Gamma>1 \<lless> \<Gamma>2"
+  and     c: "\<Gamma>1 \<subseteq> \<Gamma>2"
   shows "\<Gamma>2 \<turnstile> t : T"
 using a b c
 proof (nominal_induct \<Gamma>1 t T avoiding: \<Gamma>2 rule: typing.strong_induct)
   case (t_Lam x \<Gamma>1 T1 t T2) (* lambda case *)
   have vc: "x\<sharp>\<Gamma>2" by fact (* variable convention *)
-  have ih: "\<And>\<Gamma>3. \<lbrakk>valid \<Gamma>3; ((x,T1)#\<Gamma>1) \<lless> \<Gamma>3\<rbrakk> \<Longrightarrow>  \<Gamma>3 \<turnstile> t : T2" by fact
-  have "\<Gamma>1 \<lless> \<Gamma>2" by fact
-  then have "((x,T1)#\<Gamma>1) \<lless> ((x,T1)#\<Gamma>2)" by simp
+  have ih: "\<And>\<Gamma>3. \<lbrakk>valid \<Gamma>3; (x,T1)#\<Gamma>1 \<subseteq> \<Gamma>3\<rbrakk> \<Longrightarrow>  \<Gamma>3 \<turnstile> t : T2" by fact
+  have "\<Gamma>1 \<subseteq> \<Gamma>2" by fact
+  then have "(x,T1)#\<Gamma>1 \<subseteq> (x,T1)#\<Gamma>2" by simp
   moreover
   have "valid \<Gamma>2" by fact
   then have "valid ((x,T1)#\<Gamma>2)" using vc by (simp add: v2)
-  ultimately have "((x,T1)#\<Gamma>2) \<turnstile> t : T2" using ih by simp
-  with vc show "\<Gamma>2 \<turnstile> (Lam [x].t) : T1 \<rightarrow> T2" by auto
+  ultimately have "(x,T1)#\<Gamma>2 \<turnstile> t : T2" using ih by simp
+  with vc show "\<Gamma>2 \<turnstile> Lam [x].t : T1 \<rightarrow> T2" by auto
 qed (auto) (* app and var case *)
 
 text{* The original induction principle for the typing relation
-       is not strong enough - even this simple lemma fails:     *}
+       is not strong enough - even this simple lemma fails to be simple ;o) *}
+
 lemma weakening_too_weak: 
   assumes a: "\<Gamma>1 \<turnstile> t : T"
   and     b: "valid \<Gamma>2" 
-  and     c: "\<Gamma>1 \<lless> \<Gamma>2"
+  and     c: "\<Gamma>1 \<subseteq> \<Gamma>2"
   shows "\<Gamma>2 \<turnstile> t : T"
 using a b c
 proof (induct arbitrary: \<Gamma>2)
-  case (t_Var \<Gamma>1 x T) (* variable case *)
-  have "\<Gamma>1 \<lless> \<Gamma>2" by fact
+  case (t_Var \<Gamma>1 x T) (* variable case works *)
+  have "\<Gamma>1 \<subseteq> \<Gamma>2" by fact
   moreover
   have "valid \<Gamma>2" by fact
   moreover
@@ -134,11 +135,11 @@
   case (t_Lam x \<Gamma>1 T1 t T2) (* lambda case *)
   (* all assumptions available in this case*)
   have a0: "x\<sharp>\<Gamma>1" by fact
-  have a1: "((x,T1)#\<Gamma>1) \<turnstile> t : T2" by fact
-  have a2: "\<Gamma>1 \<lless> \<Gamma>2" by fact
+  have a1: "(x,T1)#\<Gamma>1 \<turnstile> t : T2" by fact
+  have a2: "\<Gamma>1 \<subseteq> \<Gamma>2" by fact
   have a3: "valid \<Gamma>2" by fact
-  have ih: "\<And>\<Gamma>3. \<lbrakk>valid \<Gamma>3; ((x,T1)#\<Gamma>1) \<lless> \<Gamma>3\<rbrakk>  \<Longrightarrow>  \<Gamma>3 \<turnstile> t : T2" by fact
-  have "((x,T1)#\<Gamma>1) \<lless> ((x,T1)#\<Gamma>2)" using a2 by simp
+  have ih: "\<And>\<Gamma>3. \<lbrakk>valid \<Gamma>3; (x,T1)#\<Gamma>1 \<subseteq> \<Gamma>3\<rbrakk>  \<Longrightarrow>  \<Gamma>3 \<turnstile> t : T2" by fact
+  have "(x,T1)#\<Gamma>1 \<subseteq> (x,T1)#\<Gamma>2" using a2 by simp
   moreover
   have "valid ((x,T1)#\<Gamma>2)" using v2 (* fails *) 
     oops
diff -r 6cf96b9f7b9e -r 0c5b22076fb3 src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Thu Apr 12 15:35:29 2007 +0200
+++ b/src/HOL/Nominal/Nominal.thy	Thu Apr 12 15:46:12 2007 +0200
@@ -2309,7 +2309,6 @@
   assumes pt: "pt TYPE('a) TYPE('x)"
   and     at: "at TYPE('x)"
   and     fs: "fs TYPE('a) TYPE('x)"
-  and     a: "a\<sharp>xs"
   shows "a\<sharp>(set xs) = a\<sharp>xs"
 by (simp add: fresh_def pt_list_set_supp[OF pt, OF at, OF fs])