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.
Arbitrary number of fun_map_tacs.
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Wed, 09 Dec 2009 06:21:09 +0100
changeset 657 2d9de77d5687
parent 656 c86a47d4966e
child 658 d616a0912245
child 663 0dd10a900cae
Arbitrary number of fun_map_tacs.
Quot/QuotMain.thy file | annotate | diff | comparison | revisions 
--- a/Quot/QuotMain.thy	Wed Dec 09 05:59:49 2009 +0100
+++ b/Quot/QuotMain.thy	Wed Dec 09 06:21:09 2009 +0100
@@ -1063,10 +1063,7 @@
     fun simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver
   in
     EVERY' [simp_tac (simps thms1),
-            fun_map_tac lthy,
-            fun_map_tac lthy,
-            fun_map_tac lthy,
-            fun_map_tac lthy,
+            TRY o REPEAT_ALL_NEW (CHANGED o (fun_map_tac lthy)),
             lambda_prs_tac lthy,
             simp_tac (simps thms2),
             TRY o rtac refl]
nominal2