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 61413 6d892287d0e9
parent 61268 abe08fb15a12
child 63265 9a2377b96ffd 
--- a/src/Provers/blast.ML	Mon Oct 12 20:25:08 2015 +0200
+++ b/src/Provers/blast.ML	Mon Oct 12 20:25:50 2015 +0200
@@ -18,7 +18,7 @@
   * ignores elimination rules that don't have the correct format
         (conclusion must be a formula variable)
   * rules must not require higher-order unification, e.g. apply_type in ZF
-    + message "Function Var's argument not a bound variable" relates to this
+    + message "Function unknown's argument not a bound variable" relates to this
   * its proof strategy is more general but can actually be slower
 
 Known problems:
isabelle