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.
Derivatives.thy
changeset 195 5bbe63876f84
parent 193 2a5ac68db24b
child 203 5d724fe0e096
equal deleted inserted replaced
194:5347d7556487 195:5bbe63876f84 
   267     by auto
 
   267     by auto
 
   268   also have "\<dots> \<subseteq> Timess (pder_set c (pders s r1)) r2 \<union> pder c r2 \<union> pders_lang (Suf s \<cdot> {[c]}) r2"
 
   268   also have "\<dots> \<subseteq> Timess (pder_set c (pders s r1)) r2 \<union> pder c r2 \<union> pders_lang (Suf s \<cdot> {[c]}) r2"
 
   269     by (auto simp add: if_splits) (blast)
 
   269     by (auto simp add: if_splits) (blast)
 
   270   also have "\<dots> = Timess (pders (s @ [c]) r1) r2 \<union> pder c r2 \<union> pders_lang (Suf s \<cdot> {[c]}) r2"
 
   270   also have "\<dots> = Timess (pders (s @ [c]) r1) r2 \<union> pder c r2 \<union> pders_lang (Suf s \<cdot> {[c]}) r2"
 
   271     by (simp add: pders_snoc)
 
   271     by (simp add: pders_snoc)
 
   272   also have "\<dots> \<subseteq> Timess (pders (s @ [c]) r1) r2 \<union> pders_lang (Suf (s @ [c])) r2"
 
   272   also have "\<dots> = Timess (pders (s @ [c]) r1) r2 \<union> pders_lang (Suf (s @ [c])) r2"
 
   273     unfolding pders_lang_def by (auto simp add: Suf_snoc)  
   273     unfolding pders_lang_def by (auto simp add: Suf_snoc)  
   274   finally show ?case .
 
   274   finally show ?case .
 
   275 qed (simp) 
   275 qed (simp) 
   276 
   276 
   277 lemma pders_lang_Times_aux1:
 
   277 lemma pders_lang_Times_aux1:
regexp