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/QuotMain.thy
changeset 715 3d7a9d4d2bb6
parent 704 0fd4abb5fade
child 717 337dd914e1cb
child 719 a9e55e1ef64c 
--- a/Quot/QuotMain.thy	Fri Dec 11 15:49:15 2009 +0100
+++ b/Quot/QuotMain.thy	Fri Dec 11 15:58:15 2009 +0100
@@ -1082,7 +1082,7 @@
 val msg1 = "Regularize proof failed."
 val msg2 = cat_lines ["Injection proof failed.", 
                       "This is probably due to missing respects lemmas.",
-                      "Try invoking the injection_tac manually to see", 
+                      "Try invoking the injection method manually to see", 
                       "which lemmas are missing."]
 val msg3 = "Cleaning proof failed."
nominal2