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/Equivp.thy
changeset 2108 c5b7be27f105
parent 2070 ff69913e2608
child 2288 3b83960f9544 
--- a/Nominal/Equivp.thy	Wed May 12 13:43:48 2010 +0100
+++ b/Nominal/Equivp.thy	Wed May 12 16:08:32 2010 +0200
@@ -76,7 +76,7 @@
 
 ML {*
 fun symp_tac induct inj eqvt ctxt =
-  rel_indtac induct THEN_ALL_NEW
+  rtac induct THEN_ALL_NEW
   simp_tac (HOL_basic_ss addsimps inj) THEN_ALL_NEW split_conj_tac
   THEN_ALL_NEW
   REPEAT o etac @{thm exi_neg}
@@ -111,7 +111,7 @@
 
 ML {*
 fun transp_tac ctxt induct alpha_inj term_inj distinct cases eqvt =
-  rel_indtac induct THEN_ALL_NEW
+  rtac induct THEN_ALL_NEW
   (TRY o rtac allI THEN' imp_elim_tac cases ctxt) THEN_ALL_NEW
   asm_full_simp_tac (HOL_basic_ss addsimps alpha_inj) THEN_ALL_NEW
   split_conj_tac THEN_ALL_NEW REPEAT o (eetac @{thm exi_sum} ctxt) THEN_ALL_NEW split_conj_tac
@@ -222,7 +222,7 @@
 *}
 
 ML {*
-fun fs_tac induct supports = rel_indtac induct THEN_ALL_NEW (
+fun fs_tac induct supports = rtac induct THEN_ALL_NEW (
   rtac @{thm supports_finite} THEN' resolve_tac supports) THEN_ALL_NEW
   asm_full_simp_tac (HOL_ss addsimps @{thms supp_atom supp_atom_image supp_fset_to_set
     supp_fmap_atom finite_insert finite.emptyI finite_Un finite_supp})
@@ -317,7 +317,7 @@
 
 ML {*
 fun supp_eq_tac ind fv perm eqiff ctxt =
-  rel_indtac ind THEN_ALL_NEW
+  rtac ind THEN_ALL_NEW
   asm_full_simp_tac (HOL_basic_ss addsimps fv) THEN_ALL_NEW
   asm_full_simp_tac (HOL_basic_ss addsimps @{thms supp_abs_atom[symmetric]}) THEN_ALL_NEW
   asm_full_simp_tac (HOL_basic_ss addsimps [choose_alpha_abs eqiff]) THEN_ALL_NEW
nominal2