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.
-authentic primrec
authorhaftmann
Thu, 06 Dec 2007 16:38:42 +0100
changeset 25561 d955e1d01e6a
parent 25560 63be39eeb41a
child 25562 f0fc8531c909
-authentic primrec
src/HOL/Tools/old_primrec_package.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/old_primrec_package.ML	Thu Dec 06 16:36:21 2007 +0100
+++ b/src/HOL/Tools/old_primrec_package.ML	Thu Dec 06 16:38:42 2007 +0100
@@ -17,11 +17,6 @@
     -> theory -> thm list * theory
   val add_primrec_unchecked_i: string -> ((bstring * term) * attribute list) list
     -> theory -> thm list * theory
-  (* FIXME !? *)
-  val gen_primrec: ((bstring * attribute list) * thm list -> theory -> (bstring * thm list) * theory)
-    -> ((bstring * attribute list) * term -> theory -> (bstring * thm) * theory)
-    -> string -> ((bstring * attribute list) * term) list
-    -> theory -> thm list * theory;
 end;
 
 structure OldPrimrecPackage : OLD_PRIMREC_PACKAGE =
isabelle