Mercurial Mercurial > hg > nominal2 / 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.
Nominal/nominal_dt_quot.ML
changeset 3157 de89c95c5377
parent 3060 6613514ff6cb
child 3158 89f9d7e85e88 
--- a/Nominal/nominal_dt_quot.ML	Tue Apr 10 15:21:07 2012 +0100
+++ b/Nominal/nominal_dt_quot.ML	Tue Apr 10 15:22:16 2012 +0100
@@ -11,14 +11,14 @@
   val define_qtypes: (string list * binding * mixfix) list -> typ list -> term list -> 
     thm list -> local_theory -> Quotient_Info.quotients list * local_theory
 
-  val define_qconsts: typ list -> (string  * term * mixfix) list -> local_theory -> 
+  val define_qconsts: typ list -> (string  * term * mixfix * thm) list -> local_theory -> 
     Quotient_Info.quotconsts list * local_theory
 
   val define_qperms: typ list -> string list -> (string * sort) list -> 
-    (string * term * mixfix) list -> thm list -> local_theory -> local_theory
+    (string * term * mixfix * thm) list -> thm list -> local_theory -> local_theory
 
   val define_qsizes: typ list -> string list -> (string * sort) list -> 
-    (string * term * mixfix) list -> local_theory -> local_theory
+    (string * term * mixfix * thm) list -> local_theory -> local_theory
 
   val lift_thms: typ list -> thm list -> thm list -> Proof.context -> thm list * Proof.context
nominal2