Mercurial Mercurial > hg > nominal2 / 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.
tuned
authorChristian Urban <urbanc@in.tum.de>
Wed, 09 Dec 2009 15:28:01 +0100
changeset 660 e78db03b4e11
parent 659 86c60d55373c
child 661 a0f50b34765c
tuned
Quot/QuotMain.thy file | annotate | diff | comparison | revisions 
--- a/Quot/QuotMain.thy	Wed Dec 09 15:24:11 2009 +0100
+++ b/Quot/QuotMain.thy	Wed Dec 09 15:28:01 2009 +0100
@@ -1051,10 +1051,12 @@
 thm babs_prs all_prs ex_prs 
 (* 2. unfolding of ---> in front of everything, except *)
 (*    bound variables                                  *)
-thm fun_map_simps
+thm fun_map.simps
 (* 3. simplification with *)
+lambda_prs
+(* 4. simplification with *)
 thm Quotient_abs_rep Quotient_rel_rep id_simps 
-(* 4. Test for refl *)
+(* 5. Test for refl *)
 
 ML {*
 fun clean_tac lthy =
nominal2