# HG changeset patch # User blanchet # Date 1392761337 -3600 # Node ID 0d0e19e9505ed166bb1f4f664633b0c8289cab63 # Parent d7f411651bed54db6f08825558edf92abcff7137 removed deadcode diff -r d7f411651bed -r 0d0e19e9505e src/HOL/Tools/BNF/bnf_tactics.ML --- a/src/HOL/Tools/BNF/bnf_tactics.ML Tue Feb 18 23:08:55 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_tactics.ML Tue Feb 18 23:08:57 2014 +0100 @@ -12,7 +12,6 @@ val fo_rtac: thm -> Proof.context -> int -> tactic - val mk_flatten_assoc_tac: (int -> tactic) -> thm -> thm -> thm -> tactic val mk_rotate_eq_tac: (int -> tactic) -> thm -> thm -> thm -> thm -> ''a list -> ''a list -> int -> tactic @@ -21,8 +20,6 @@ val mk_Abs_bij_thm: Proof.context -> thm -> thm -> thm val mk_Abs_inj_thm: thm -> thm - val mk_ctor_or_dtor_rel_tac: Proof.context -> thm -> thm list -> thm list -> thm -> tactic - val mk_map_comp_id_tac: thm -> tactic val mk_map_cong0_tac: Proof.context -> int -> thm -> tactic val mk_map_cong0L_tac: int -> thm -> thm -> tactic @@ -85,15 +82,6 @@ gen_tac end; -fun mk_ctor_or_dtor_rel_tac ctxt srel_def IJrel_defs IJsrel_defs dtor_srel = - unfold_thms_tac ctxt IJrel_defs THEN - rtac (unfold_thms ctxt (IJrel_defs @ IJsrel_defs @ - @{thms Collect_mem_eq mem_Collect_eq fst_conv snd_conv}) dtor_srel RS trans) 1 THEN - unfold_thms_tac ctxt (srel_def :: - @{thms pair_collapse Collect_mem_eq mem_Collect_eq prod.cases fst_conv snd_conv - split_conv}) THEN - rtac refl 1; - fun mk_map_comp_id_tac map_comp0 = (rtac trans THEN' rtac map_comp0 THEN' REPEAT_DETERM o stac @{thm comp_id} THEN' rtac refl) 1;