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.
Quot/quotient_term.ML
changeset 782 86c7ed9f354f
parent 779 3b21b24a5fb6
child 783 06e17083e90b 
--- a/Quot/quotient_term.ML	Wed Dec 23 13:45:42 2009 +0100
+++ b/Quot/quotient_term.ML	Wed Dec 23 21:30:23 2009 +0100
@@ -287,8 +287,9 @@
   
   * If the application involves a bounded quantifier, we recurse on 
     the second argument. If the application is a bounded abstraction,
-    we always put an Re/Abs around it (since bounded abstractions
-    always need lifting). Otherwise we recurse on both arguments.
+    we always put an Rep/Abs around it (since bounded abstractions
+    are assumed to always need lifting). Otherwise we recurse on both 
+    arguments.
 
   For constants:
nominal2