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/Nominal2.thy
changeset 2650 e5fa8de0e4bd
parent 2649 a8ebcb368a15
child 2665 16b5a67ee279 
--- a/Nominal/Nominal2.thy	Thu Jan 06 23:06:45 2011 +0000
+++ b/Nominal/Nominal2.thy	Fri Jan 07 02:30:00 2011 +0000
@@ -250,7 +250,7 @@
   val lthy5 = snd (Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_fv_eqvt) lthy_tmp)
 
   val (alpha_eqvt, lthy6) =
-    Nominal_Eqvt.equivariance true (alpha_trms @ alpha_bn_trms) alpha_induct alpha_intros lthy5
+    Nominal_Eqvt.raw_equivariance true (alpha_trms @ alpha_bn_trms) alpha_induct alpha_intros lthy5
 
   val _ = trace_msg (K "Proving equivalence of alpha...")
   val alpha_refl_thms =
nominal2