1.1 --- a/src/HOL/Nominal/Examples/Weakening.thy	Fri Nov 17 02:19:55 2006 +0100
     1.2 +++ b/src/HOL/Nominal/Examples/Weakening.thy	Fri Nov 17 02:20:03 2006 +0100
     1.3 @@ -193,7 +193,7 @@
     1.4  text {* definition of a subcontext *}
     1.5  
     1.6  abbreviation
     1.7 -  "sub" :: "(name\<times>ty) list \<Rightarrow> (name\<times>ty) list \<Rightarrow> bool" (" _ \<lless> _ " [80,80] 80)
     1.8 +  "sub" :: "(name\<times>ty) list \<Rightarrow> (name\<times>ty) list \<Rightarrow> bool" (" _ \<lless> _ " [80,80] 80) where
     1.9    "\<Gamma>1 \<lless> \<Gamma>2 \<equiv> \<forall>a \<sigma>. (a,\<sigma>)\<in>set \<Gamma>1 \<longrightarrow> (a,\<sigma>)\<in>set \<Gamma>2"
    1.10  
    1.11  text {* Now it comes: The Weakening Lemma *}