16   val addposts : (eqvt_config * thm list) -> eqvt_config

    16   val addposts : (eqvt_config * thm list) -> eqvt_config

    17   val addexcls : (eqvt_config * string list) -> eqvt_config

    17   val addexcls : (eqvt_config * string list) -> eqvt_config

    18   val delpres : eqvt_config -> eqvt_config

    18   val delpres : eqvt_config -> eqvt_config

    19   val delposts : eqvt_config -> eqvt_config

    19   val delposts : eqvt_config -> eqvt_config

    20 

    20 

    21   val eqvt_rule: Proof.context -> eqvt_config -> thm -> thm

    22   val eqvt_rule: Proof.context -> eqvt_config -> thm -> thm

    22   val eqvt_tac: Proof.context -> eqvt_config -> int -> tactic

    23   val eqvt_tac: Proof.context -> eqvt_config -> int -> tactic

    23 

    24 

    24   val perm_simp_meth: thm list * string list -> Proof.context -> Method.method

    25   val perm_simp_meth: thm list * string list -> Proof.context -> Method.method

    25   val perm_strict_simp_meth: thm list * string list -> Proof.context -> Method.method

    26   val perm_strict_simp_meth: thm list * string list -> Proof.context -> Method.method