Mercurial Mercurial > repos > isabelle / 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.
src/Provers/blast.ML
changeset 15661 9ef583b08647
parent 15574 b1d1b5bfc464
child 15786 81e9f17823ea 
--- a/src/Provers/blast.ML	Thu Apr 07 09:24:35 2005 +0200
+++ b/src/Provers/blast.ML	Thu Apr 07 09:25:33 2005 +0200
@@ -24,7 +24,7 @@
   "Recursive" chains of rules can sometimes exclude other unsafe formulae
 	from expansion.  This happens because newly-created formulae always
 	have priority over existing ones.  But obviously recursive rules 
-	such as transitivity are treated specially to prevent this.  SOMEtimes
+	such as transitivity are treated specially to prevent this.  Sometimes
 	the formulae get into the wrong order (see WRONG below).
 
   With substition for equalities (hyp_subst_tac):
isabelle