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.
quotient_info.ML
changeset 322 d741ccea80d3
parent 321 f46dc0ca08c3
child 324 bdbb52979790 
--- a/quotient_info.ML	Sat Nov 21 02:49:39 2009 +0100
+++ b/quotient_info.ML	Sat Nov 21 02:53:23 2009 +0100
@@ -12,6 +12,7 @@
   val quotdata_update_thy: string -> (typ * typ * term * thm) -> theory -> theory
   val quotdata_update: string -> (typ * typ * term * thm) -> Proof.context -> Proof.context
 
+  (*FIXME: obsolete *)
   type qenv = (typ * typ) list
   val mk_qenv: Proof.context -> qenv
   val lookup_qenv: ((typ * typ) -> bool) -> qenv -> typ -> (typ * typ) option
nominal2