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>
Thu, 03 Feb 2011 02:57:04 +0000
changeset 2717 e8c1a19e13d2
parent 2716 cd336163f270 (diff)
parent 2715 08bc1aa259d9 (current diff)
child 2718 8c1cda7ec284
merged
--- a/Nominal/nominal_function_core.ML	Tue Feb 01 09:07:55 2011 +0900
+++ b/Nominal/nominal_function_core.ML	Thu Feb 03 02:57:04 2011 +0000
@@ -483,9 +483,6 @@
       |> 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