src/Provers/induct_method.ML
changeset 18708 4b3dadb4fe33
parent 18678 dd0c569fa43d
child 18799 f137c5e971f5
     1.1 --- a/src/Provers/induct_method.ML	Thu Jan 19 15:45:10 2006 +0100
     1.2 +++ b/src/Provers/induct_method.ML	Thu Jan 19 21:22:08 2006 +0100
     1.3 @@ -32,7 +32,7 @@
     1.4      cases_tactic
     1.5    val coinduct_tac: Proof.context -> bool -> term option list -> term option list ->
     1.6      thm option -> thm list -> int -> cases_tactic
     1.7 -  val setup: (theory -> theory) list
     1.8 +  val setup: theory -> theory
     1.9  end;
    1.10  
    1.11  functor InductMethodFun(Data: INDUCT_METHOD_DATA): INDUCT_METHOD =
    1.12 @@ -556,9 +556,9 @@
    1.13  (** theory setup **)
    1.14  
    1.15  val setup =
    1.16 -  [Method.add_methods
    1.17 +  Method.add_methods
    1.18      [(InductAttrib.casesN, cases_meth, "case analysis on types or sets"),
    1.19       (InductAttrib.inductN, induct_meth, "induction on types or sets"),
    1.20 -     (InductAttrib.coinductN, coinduct_meth, "coinduction on types or sets")]];
    1.21 +     (InductAttrib.coinductN, coinduct_meth, "coinduction on types or sets")];
    1.22  
    1.23  end;