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/Rsp.thy
changeset 2029 e72121ea134b
parent 1898 f8c8e2afcc18
child 2072 db218886e674
equal deleted inserted replaced
2028:15c5a2926622 2029:e72121ea134b 
    95 
    95 
    96 
    96 
    97 ML {*
 
    97 ML {*
 
    98 fun alpha_eqvt_tac induct simps ctxt =
 
    98 fun alpha_eqvt_tac induct simps ctxt =
 
    99   rel_indtac induct THEN_ALL_NEW
 
    99   rel_indtac induct THEN_ALL_NEW
 
   100   simp_tac (HOL_basic_ss addsimps simps) THEN_ALL_NEW
 
   100   simp_tac (HOL_basic_ss addsimps simps) THEN_ALL_NEW split_conj_tac THEN_ALL_NEW
 
   101   REPEAT o etac @{thm exi[of _ _ "p"]} THEN' split_conj_tac THEN_ALL_NEW
 
   101   REPEAT o etac @{thm exi[of _ _ "p"]} THEN' split_conj_tac THEN_ALL_NEW
 
   102   asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ simps)) THEN_ALL_NEW
 
   102   asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ simps)) THEN_ALL_NEW
 
   103   asm_full_simp_tac (HOL_ss addsimps 
   103   asm_full_simp_tac (HOL_ss addsimps 
   104     @{thms supp_eqvt[symmetric] inter_eqvt[symmetric] empty_eqvt alphas}) THEN_ALL_NEW
 
   104     @{thms supp_eqvt[symmetric] inter_eqvt[symmetric] empty_eqvt alphas}) THEN_ALL_NEW
 
   105   (split_conj_tac THEN_ALL_NEW TRY o resolve_tac
 
   105   (split_conj_tac THEN_ALL_NEW TRY o resolve_tac
nominal2