Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Replaced xstring by thmref.
authorberghofe
Mon, 24 Jan 2005 18:07:10 +0100
changeset 15458 9c292e3e0ca1
parent 15457 1fbd4aba46e3
child 15459 16dd63c78049
Replaced xstring by thmref.
src/HOL/Tools/recdef_package.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/recdef_package.ML	Mon Jan 24 17:59:48 2005 +0100
+++ b/src/HOL/Tools/recdef_package.ML	Mon Jan 24 18:07:10 2005 +0100
@@ -31,7 +31,7 @@
   val add_recdef_old: xstring -> string -> ((bstring * string) * Args.src list) list ->
     simpset * thm list -> theory ->
     theory * {simps: thm list, rules: thm list list, induct: thm, tcs: term list}
-  val defer_recdef: xstring -> string list -> (xstring * Args.src list) list
+  val defer_recdef: xstring -> string list -> (thmref * Args.src list) list
     -> theory -> theory * {induct_rules: thm}
   val defer_recdef_i: xstring -> term list -> (thm list * theory attribute list) list
     -> theory -> theory * {induct_rules: thm}
isabelle