--- a/src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML Mon Aug 12 09:51:00 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML Mon Aug 12 15:25:16 2013 +0200
@@ -36,7 +36,7 @@
fun mk_nchotomy_tac n exhaust =
HEADGOAL (rtac allI THEN' rtac exhaust THEN'
- EVERY' (maps (fn k => [rtac (mk_disjIN n k), REPEAT_DETERM o rtac exI, atac]) (1 upto n)));
+ EVERY' (maps (fn k => [rtac (mk_disjIN n k), REPEAT_DETERM o rtac exI, atac]) (1 upto n)));
fun mk_unique_disc_def_tac m uexhaust =
HEADGOAL (EVERY' [rtac iffI, rtac uexhaust, REPEAT_DETERM_N m o rtac exI, atac, rtac refl]);
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML Mon Aug 12 09:51:00 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML Mon Aug 12 15:25:16 2013 +0200
@@ -149,7 +149,7 @@
mss (unflat mss (1 upto n)) kkss)
end;
-fun mk_coinduct_same_ctr ctxt rel_eqs pre_rel_def dtor_ctor ctr_def discs sels =
+fun mk_coinduct_same_ctr_tac ctxt rel_eqs pre_rel_def dtor_ctor ctr_def discs sels =
hyp_subst_tac ctxt THEN'
CONVERSION (hhf_concl_conv
(Conv.top_conv (K (Conv.try_conv (Conv.rewr_conv ctr_def))) ctxt) ctxt) THEN'
@@ -161,7 +161,7 @@
REPEAT o etac conjE THEN_MAYBE' REPEAT o hyp_subst_tac ctxt THEN' REPEAT o rtac conjI THEN'
REPEAT o rtac refl);
-fun mk_coinduct_distinct_ctrs ctxt discs discs' =
+fun mk_coinduct_distinct_ctrs_tac ctxt discs discs' =
hyp_subst_tac ctxt THEN' REPEAT o etac conjE THEN'
full_simp_tac (ss_only (refl :: no_refl (discs @ discs') @ basic_simp_thms) ctxt);
@@ -175,9 +175,9 @@
EVERY' ([rtac exhaust, K (inst_as_projs_tac ctxt 2)] @
map2 (fn k' => fn discs' =>
if k' = k then
- mk_coinduct_same_ctr ctxt rel_eqs' pre_rel_def dtor_ctor ctr_def discs sels
+ mk_coinduct_same_ctr_tac ctxt rel_eqs' pre_rel_def dtor_ctor ctr_def discs sels
else
- mk_coinduct_distinct_ctrs ctxt discs discs') ks discss)) ks ctr_defs discss selss)
+ mk_coinduct_distinct_ctrs_tac ctxt discs discs') ks discss)) ks ctr_defs discss selss)
end;
fun mk_coinduct_tac ctxt rel_eqs' nn ns dtor_coinduct' pre_rel_defs dtor_ctors exhausts ctr_defss