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.
ML signature interface
authorhaftmann
Wed, 17 Nov 2010 11:27:48 +0100
changeset 40584 28cc2acbc58a
parent 40583 6fed6f946471
child 40585 e14bbfee8804
ML signature interface
src/HOL/Tools/functorial_mappers.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/functorial_mappers.ML	Wed Nov 17 11:26:39 2010 +0100
+++ b/src/HOL/Tools/functorial_mappers.ML	Wed Nov 17 11:27:48 2010 +0100
@@ -11,6 +11,7 @@
     -> bool -> typ -> typ -> term
   val register: string -> string -> (sort * (bool * bool)) list -> thm -> thm
     -> theory -> theory
+  val type_mapper: term -> theory -> Proof.state
   type entry
   val entries: theory -> entry Symtab.table
 end;
isabelle