Mercurial Mercurial > hg > nominal2 / 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.
merged
authorChristian Urban <urbanc@in.tum.de>
Fri, 04 Dec 2009 11:34:49 +0100
changeset 521 fdfeef0399f7
parent 520 cc1f240d8cf4 (diff)
parent 519 ebfd747b47ab (current diff)
child 523 1a4eb39ba834
merged
QuotMain.thy file | annotate | diff | comparison | revisions 
--- a/QuotMain.thy	Fri Dec 04 11:33:58 2009 +0100
+++ b/QuotMain.thy	Fri Dec 04 11:34:49 2009 +0100
@@ -795,7 +795,7 @@
               val [R2, f, g, x, y] = map (cterm_of thy) [R2, f, g, x, y];
               val t_inst = [NONE, NONE, NONE, SOME R2, NONE, NONE, SOME f, SOME g, SOME x, SOME y];
               val thm = Drule.instantiate' ty_inst t_inst @{thm APPLY_RSP}
-              (*val _ = tracing (Syntax.string_of_term @{context} (prop_of thm))*)
+              val _ = tracing ("instantiated rule" ^ Syntax.string_of_term @{context} (prop_of thm))
             in
               rtac thm 1
             end
nominal2