Mercurial Mercurial > hg > regexp / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
small typo
authorurbanc
Fri, 12 Aug 2011 17:08:58 +0000
changeset 195 5bbe63876f84
parent 194 5347d7556487
child 196 fa8d33d13cb6
small typo
Derivatives.thy file | annotate | diff | comparison | revisions 
--- 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