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_Eqvt.thy
changeset 1326 4bc9278a808d
parent 1315 43d6e3730353
child 1331 0f329449e304 
--- a/Nominal/Nominal2_Eqvt.thy	Wed Mar 03 10:39:43 2010 +0100
+++ b/Nominal/Nominal2_Eqvt.thy	Wed Mar 03 11:42:15 2010 +0100
@@ -239,7 +239,8 @@
   imp_eqvt [folded induct_implies_def]
 
   (* nominal *)
-  permute_eqvt supp_eqvt fresh_eqvt
+  (*permute_eqvt commented out since it loops *)
+  supp_eqvt fresh_eqvt
   permute_pure
 
   (* datatypes *)
nominal2