diff -r 5347d7556487 -r 5bbe63876f84 Derivatives.thy
--- 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)