clarified IsarThy.apply_theorems_i;
authorwenzelm
Fri Jan 11 00:28:24 2002 +0100 (2002-01-11 ago)
changeset 1270831672377dadc
parent 12707 4013be8572c5
child 12709 e29800eba5d1
clarified IsarThy.apply_theorems_i;
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/recdef_package.ML
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Fri Jan 11 00:27:40 2002 +0100
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Fri Jan 11 00:28:24 2002 +0100
     1.3 @@ -40,8 +40,9 @@
     1.4         induction : thm,
     1.5         size : thm list,
     1.6         simps : thm list}
     1.7 -  val rep_datatype_i : string list option -> (thm * theory attribute list) list list ->
     1.8 -    (thm * theory attribute list) list list -> (thm * theory attribute list) -> theory -> theory *
     1.9 +  val rep_datatype_i : string list option -> (thm list * theory attribute list) list list ->
    1.10 +    (thm list * theory attribute list) list list -> (thm list * theory attribute list) ->
    1.11 +    theory -> theory *
    1.12        {distinct : thm list list,
    1.13         inject : thm list list,
    1.14         exhaustion : thm list,
     2.1 --- a/src/HOL/Tools/recdef_package.ML	Fri Jan 11 00:27:40 2002 +0100
     2.2 +++ b/src/HOL/Tools/recdef_package.ML	Fri Jan 11 00:28:24 2002 +0100
     2.3 @@ -34,7 +34,7 @@
     2.4      theory * {simps: thm list, rules: thm list list, induct: thm, tcs: term list}
     2.5    val defer_recdef: xstring -> string list -> (xstring * Args.src list) list
     2.6      -> theory -> theory * {induct_rules: thm}
     2.7 -  val defer_recdef_i: xstring -> term list -> (thm * theory attribute list) list
     2.8 +  val defer_recdef_i: xstring -> term list -> (thm list * theory attribute list) list
     2.9      -> theory -> theory * {induct_rules: thm}
    2.10    val recdef_tc: bstring * Args.src list -> xstring -> int option
    2.11      -> bool -> theory -> ProofHistory.T