Mercurial Mercurial > hg > nominal2 / 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.
flagged qenv-stuff as obsolete
authorChristian Urban <urbanc@in.tum.de>
Sat, 21 Nov 2009 02:53:23 +0100
changeset 322 d741ccea80d3
parent 321 f46dc0ca08c3
child 323 31509c8cf72e
flagged qenv-stuff as obsolete
quotient_info.ML file | annotate | diff | comparison | revisions 
--- 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