Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/BNF/Tools/bnf_util.ML
changeset 53037 e5fa456890b4
parent 53036 7dd103c29f9d
child 53038 dd5ea8a51af0 
--- a/src/HOL/BNF/Tools/bnf_util.ML	Fri Aug 16 18:14:58 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_util.ML	Fri Aug 16 18:36:55 2013 +0200
@@ -78,6 +78,7 @@
   val binder_fun_types: typ -> typ list
   val body_fun_type: typ -> typ
   val num_binder_types: typ -> int
+  val strip_fun_type: typ -> typ list * typ
   val strip_typeN: int -> typ -> typ list * typ
 
   val mk_predT: typ list -> typ
isabelle