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.
improved tracing of permutative rules.
authornipkow
Thu, 10 May 2001 17:28:40 +0200
changeset 11295 66925f23ac7f
parent 11294 16481a4cc9f3
child 11296 38a69e5d79fa
improved tracing of permutative rules.
src/Pure/meta_simplifier.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/meta_simplifier.ML	Thu May 10 13:44:44 2001 +0200
+++ b/src/Pure/meta_simplifier.ML	Thu May 10 17:28:40 2001 +0200
@@ -584,7 +584,9 @@
         val unconditional = (Logic.count_prems (prop',0) = 0);
         val (lhs', rhs') = Logic.dest_equals (Logic.strip_imp_concl prop')
       in
-        if perm andalso not (termless (rhs', lhs')) then None
+        if perm andalso not (termless (rhs', lhs'))
+        then (trace_thm false "Cannot apply permutative rewrite rule:" thm;
+              trace_thm false "Term does not become smaller:" thm'; None)
         else
           (trace_thm false "Applying instance of rewrite rule:" thm;
            if unconditional
isabelle