Mercurial Mercurial > hg > regexp / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Closures.thy
changeset 193 2a5ac68db24b
parent 191 f6a603be52d6
child 200 204856ef5573
equal deleted inserted replaced
192:ce24ed955cca 193:2a5ac68db24b 
   141 qed
 
   141 qed
 
   142   
   142   
   143 subsection {* Closure under left-quotients *}
 
   143 subsection {* Closure under left-quotients *}
 
   144 
   144 
   145 abbreviation
 
   145 abbreviation
 
   146   "Ders_lang A B \<equiv> \<Union>s \<in> A. Ders s B"
 
   146   "Ders_lang A B \<equiv> \<Union>x \<in> A. Ders x B"
 
   147 
   147 
   148 lemma closure_left_quotient:
 
   148 lemma closure_left_quotient:
 
   149   assumes "regular A"
 
   149   assumes "regular A"
 
   150   shows "regular (Ders_lang B A)"
 
   150   shows "regular (Ders_lang B A)"
 
   151 proof -
 
   151 proof -
regexp