src/ZF/Tools/induct_tacs.ML
changeset 15703 727ef1b8b3ee
parent 15574 b1d1b5bfc464
child 15705 b5edb9dcec9a
     1.1 --- a/src/ZF/Tools/induct_tacs.ML	Wed Apr 13 09:48:41 2005 +0200
     1.2 +++ b/src/ZF/Tools/induct_tacs.ML	Wed Apr 13 18:34:22 2005 +0200
     1.3 @@ -13,8 +13,8 @@
     1.4    val induct_tac: string -> int -> tactic
     1.5    val exhaust_tac: string -> int -> tactic
     1.6    val rep_datatype_i: thm -> thm -> thm list -> thm list -> theory -> theory
     1.7 -  val rep_datatype: thmref * Args.src list -> thmref * Args.src list ->
     1.8 -    (thmref * Args.src list) list -> (thmref * Args.src list) list -> theory -> theory
     1.9 +  val rep_datatype: thmref * Attrib.src list -> thmref * Attrib.src list ->
    1.10 +    (thmref * Attrib.src list) list -> (thmref * Attrib.src list) list -> theory -> theory
    1.11    val setup: (theory -> theory) list
    1.12  end;
    1.13