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/NewParser.thy
changeset 2313 25d2cdf7d7e4
parent 2311 4da5c5c29009
child 2314 1a14c4171a51 
--- a/Nominal/NewParser.thy	Mon Jun 07 11:46:26 2010 +0200
+++ b/Nominal/NewParser.thy	Wed Jun 09 15:14:16 2010 +0200
@@ -427,6 +427,8 @@
 
   val _ = tracing ("alphas " ^ commas (map (Syntax.string_of_term lthy4) alpha_trms))
   val _ = tracing ("alpha_bns " ^ commas (map (Syntax.string_of_term lthy4) alpha_bn_trms))
+  val _ = tracing ("alpha_trans\n" ^ 
+    cat_lines (map (Syntax.string_of_term lthy4 o prop_of) alpha_trans_thms))
 
   val _ = 
     if get_STEPS lthy > 11
nominal2