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.
tuned comments;
authorwenzelm
Thu, 07 Dec 2023 09:34:07 +0100
changeset 79162 c1bbaa0d89b4
parent 79161 3f532c76d0ad
child 79163 9ddcaca41ed2
tuned comments;
src/Pure/cterm_items.ML file | annotate | diff | comparison | revisions
src/Pure/unify.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/cterm_items.ML	Wed Dec 06 22:03:14 2023 +0100
+++ b/src/Pure/cterm_items.ML	Thu Dec 07 09:34:07 2023 +0100
@@ -2,7 +2,7 @@
     Author:     Makarius
 
 Scalable collections of term items: for type thm and cterm.
-See als Pure/term_items.ML.
+See also Pure/term_items.ML.
 *)
 
 structure Ctermtab:
--- a/src/Pure/unify.ML	Wed Dec 06 22:03:14 2023 +0100
+++ b/src/Pure/unify.ML	Thu Dec 07 09:34:07 2023 +0100
@@ -68,7 +68,7 @@
 (*OCCURS CHECK
   Does the uvar occur in the term t?
   two forms of search, for whether there is a rigid path to the current term.
-  "seen" is list of variables passed thru, is a memo variable for sharing.
+  "seen" is list of variables passed through, is a memo variable for sharing.
   This version searches for nonrigid occurrence, returns true if found.
   Since terms may contain variables with same name and different types,
   the occurs check must ignore the types of variables. This avoids
isabelle