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.
nicer warning message for indirect-recursive domain definitions
authorhuffman
Thu, 19 Nov 2009 22:28:36 -0800
changeset 33810 38375b16ffd9
parent 33809 033831fd9ef3
child 33811 b1b66441275d
nicer warning message for indirect-recursive domain definitions
src/HOLCF/Tools/Domain/domain_theorems.ML file | annotate | diff | comparison | revisions 
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu Nov 19 22:25:11 2009 -0800
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu Nov 19 22:28:36 2009 -0800
@@ -998,7 +998,7 @@
       handle THM _ =>
              (warning "Induction proofs failed (THM raised)."; ([], TrueI))
            | ERROR _ =>
-             (warning "Induction proofs failed (ERROR raised)."; ([], TrueI));
+             (warning "Cannot prove induction rule"; ([], TrueI));
 
 
 end; (* local *)
isabelle