equal
deleted
inserted
replaced
191 |
191 |
192 |
192 |
193 text {* definition of a subcontext *} |
193 text {* definition of a subcontext *} |
194 |
194 |
195 abbreviation |
195 abbreviation |
196 "sub" :: "(name\<times>ty) list \<Rightarrow> (name\<times>ty) list \<Rightarrow> bool" (" _ \<lless> _ " [80,80] 80) |
196 "sub" :: "(name\<times>ty) list \<Rightarrow> (name\<times>ty) list \<Rightarrow> bool" (" _ \<lless> _ " [80,80] 80) where |
197 "\<Gamma>1 \<lless> \<Gamma>2 \<equiv> \<forall>a \<sigma>. (a,\<sigma>)\<in>set \<Gamma>1 \<longrightarrow> (a,\<sigma>)\<in>set \<Gamma>2" |
197 "\<Gamma>1 \<lless> \<Gamma>2 \<equiv> \<forall>a \<sigma>. (a,\<sigma>)\<in>set \<Gamma>1 \<longrightarrow> (a,\<sigma>)\<in>set \<Gamma>2" |
198 |
198 |
199 text {* Now it comes: The Weakening Lemma *} |
199 text {* Now it comes: The Weakening Lemma *} |
200 |
200 |
201 lemma weakening_version1: |
201 lemma weakening_version1: |