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.
Nominal/nominal_dt_alpha.ML
changeset 3029 6fd3fc3254ee
parent 2957 01ff621599bc
child 3045 d0ad264f8c4f 
--- a/Nominal/nominal_dt_alpha.ML	Wed Sep 21 17:16:11 2011 +0900
+++ b/Nominal/nominal_dt_alpha.ML	Wed Sep 21 10:23:06 2011 +0200
@@ -564,7 +564,7 @@
         [ etac @{thm exE},
           etac @{thm exE},
           perm_inst_tac ctxt, 
-          resolve_tac @{thms alpha_trans_eqvt}, 
+          resolve_tac @{thms alpha_trans_eqvt},
           atac,
           aatac pred_names ctxt, 
           eqvt_tac ctxt (eqvt_relaxed_config addpres alpha_eqvt) THEN' rtac @{thm refl},
nominal2