src/HOL/BNF/Tools/bnf_gfp_tactics.ML
changeset 49516 d4859efc1096
parent 49510 ba50d204095e
child 49541 32fb6e4c7f4b
     1.1 --- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Fri Sep 21 18:25:17 2012 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Fri Sep 21 18:25:17 2012 +0200
     1.3 @@ -38,6 +38,8 @@
     1.4    val mk_corec_tac: int -> thm list -> thm -> thm -> thm list ->
     1.5      {prems: 'a, context: Proof.context} -> tactic
     1.6    val mk_dtor_coinduct_tac: int -> int list -> thm -> thm -> tactic
     1.7 +  val mk_dtor_srel_tac: thm list -> int -> thm -> thm -> thm -> thm -> thm list -> thm -> thm ->
     1.8 +    thm list -> thm list -> thm list list -> tactic
     1.9    val mk_dtor_strong_coinduct_tac: int list -> ctyp option list -> cterm option list -> thm ->
    1.10      thm -> thm -> tactic
    1.11    val mk_dtor_o_ctor_tac: thm -> thm -> thm -> thm -> thm list ->
    1.12 @@ -109,8 +111,6 @@
    1.13    val mk_srel_coinduct_tac: 'a list -> thm -> thm -> tactic
    1.14    val mk_srel_strong_coinduct_tac: int -> ctyp option list -> cterm option list -> thm ->
    1.15      thm list -> thm list -> tactic
    1.16 -  val mk_srel_simp_tac: thm list -> int -> thm -> thm -> thm -> thm -> thm list -> thm -> thm ->
    1.17 -    thm list -> thm list -> thm list list -> tactic
    1.18    val mk_strT_hset_tac: int -> int -> int -> ctyp option list -> ctyp option list ->
    1.19      cterm option list -> thm list -> thm list -> thm list -> thm list -> thm list list ->
    1.20      thm list list -> thm list list -> thm -> thm list list -> tactic
    1.21 @@ -1494,7 +1494,7 @@
    1.22    ALLGOALS (TRY o
    1.23      FIRST' [rtac TrueI, rtac refl, etac (refl RSN (2, mp)), dresolve_tac wits THEN' etac FalseE])
    1.24  
    1.25 -fun mk_srel_simp_tac in_Jsrels i in_srel map_comp map_cong map_simp set_simps dtor_inject dtor_ctor
    1.26 +fun mk_dtor_srel_tac in_Jsrels i in_srel map_comp map_cong map_simp set_simps dtor_inject dtor_ctor
    1.27    set_naturals set_incls set_set_inclss =
    1.28    let
    1.29      val m = length set_incls;