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.
clarified error message
authorkrauss
Wed, 13 Dec 2006 14:56:50 +0100
changeset 21817 0210a5db2013
parent 21816 453fd9857b4c
child 21818 4d2ad5445c81
clarified error message
src/HOL/Tools/function_package/lexicographic_order.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/function_package/lexicographic_order.ML	Wed Dec 13 14:54:07 2006 +0100
+++ b/src/HOL/Tools/function_package/lexicographic_order.ML	Wed Dec 13 14:56:50 2006 +0100
@@ -224,7 +224,7 @@
     val possible_order = search_table table
       in
     case possible_order of 
-        NONE => error (cat_lines ("Could not prove it by lexicographic order:"::(pr_err table thy tl base_funs)))
+        NONE => error (cat_lines ("Could not find lexicographic termination order:"::(pr_err table thy tl base_funs)))
       | SOME order  => let
       val clean_table = map (fn x => map (nth x) order) table
       val funs = map (nth base_funs) order
isabelle