Mercurial Mercurial > hg > nominal2 / comparison
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
equal deleted inserted replaced
3027:aa5059a00f41 3029:6fd3fc3254ee 
   562     THEN_ALL_NEW (asm_simp_tac HOL_basic_ss THEN' 
   562     THEN_ALL_NEW (asm_simp_tac HOL_basic_ss THEN' 
   563       TRY o EVERY'   (* if binders are present *)
 
   563       TRY o EVERY'   (* if binders are present *)
 
   564         [ etac @{thm exE},
 
   564         [ etac @{thm exE},
 
   565           etac @{thm exE},
 
   565           etac @{thm exE},
 
   566           perm_inst_tac ctxt, 
   566           perm_inst_tac ctxt, 
   567           resolve_tac @{thms alpha_trans_eqvt}, 
   567           resolve_tac @{thms alpha_trans_eqvt},
 
   568           atac,
 
   568           atac,
 
   569           aatac pred_names ctxt, 
   569           aatac pred_names ctxt, 
   570           eqvt_tac ctxt (eqvt_relaxed_config addpres alpha_eqvt) THEN' rtac @{thm refl},
 
   570           eqvt_tac ctxt (eqvt_relaxed_config addpres alpha_eqvt) THEN' rtac @{thm refl},
 
   571           asm_full_simp_tac (HOL_ss addsimps prod_simps) ])
 
   571           asm_full_simp_tac (HOL_ss addsimps prod_simps) ])
 
   572   end
 
   572   end
nominal2