Mercurial Mercurial > hg > regexp / diff
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 
--- a/Derivatives.thy	Thu Aug 11 23:42:06 2011 +0000
+++ b/Derivatives.thy	Fri Aug 12 17:08:58 2011 +0000
@@ -269,7 +269,7 @@
     by (auto simp add: if_splits) (blast)
   also have "\<dots> = Timess (pders (s @ [c]) r1) r2 \<union> pder c r2 \<union> pders_lang (Suf s \<cdot> {[c]}) r2"
     by (simp add: pders_snoc)
-  also have "\<dots> \<subseteq> Timess (pders (s @ [c]) r1) r2 \<union> pders_lang (Suf (s @ [c])) r2"
+  also have "\<dots> = Timess (pders (s @ [c]) r1) r2 \<union> pders_lang (Suf (s @ [c])) r2"
     unfolding pders_lang_def by (auto simp add: Suf_snoc)  
   finally show ?case .
 qed (simp)
regexp