Mercurial Mercurial > hg > nominal2 / 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.
Quot/QuotMain.thy
changeset 661 a0f50b34765c
parent 660 e78db03b4e11
child 662 37de94a84dbc 
--- a/Quot/QuotMain.thy	Wed Dec 09 15:28:01 2009 +0100
+++ b/Quot/QuotMain.thy	Wed Dec 09 15:29:36 2009 +0100
@@ -1053,7 +1053,7 @@
 (*    bound variables                                  *)
 thm fun_map.simps
 (* 3. simplification with *)
-lambda_prs
+thm lambda_prs
 (* 4. simplification with *)
 thm Quotient_abs_rep Quotient_rel_rep id_simps 
 (* 5. Test for refl *)
nominal2