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.
Closures.thy
changeset 191 f6a603be52d6
parent 190 b73478aaf33e
child 193 2a5ac68db24b 
--- a/Closures.thy	Tue Aug 09 22:15:11 2011 +0000
+++ b/Closures.thy	Thu Aug 11 10:26:19 2011 +0000
@@ -153,7 +153,7 @@
   have fin: "finite (pders_lang B r)" by (rule finite_pders_lang)
   
   have "Ders_lang B (lang r) = (\<Union> lang ` (pders_lang B r))"
-    by (simp add: Ders_pders)
+    by (simp add: Ders_pders pders_lang_def)
   also have "\<dots> = lang (\<Uplus>(pders_lang B r))" using fin by simp
   finally have "Ders_lang B A = lang (\<Uplus>(pders_lang B r))" using eq
     by simp
regexp