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.
Nominal/nominal_function_core.ML
changeset 2709 eb4a2f4078ae
parent 2707 747ebf2f066d
child 2716 cd336163f270 
--- a/Nominal/nominal_function_core.ML	Thu Jan 27 04:24:17 2011 +0100
+++ b/Nominal/nominal_function_core.ML	Thu Jan 27 20:19:13 2011 +0100
@@ -482,6 +482,9 @@
     val ih_elim = ihyp_thm RS (f_def RS ex1_implies_un)
       |> instantiate' [] [NONE, SOME (cterm_of thy h)]
     val ih_eqvt = ihyp_thm RS (G_eqvt RS (f_def RS @{thm fundef_ex1_eqvt_at}))
+ 
+    val _ = tracing ("ihyp_thm\n" ^ @{make_string} ihyp_thm)
+    val _ = tracing ("ih_eqvt\n" ^ @{make_string} ih_eqvt)
 
     val _ = trace_msg (K "Proving Replacement lemmas...")
     val repLemmas = map (mk_replacement_lemma thy h ih_elim) clauses
nominal2