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.
fixed (permute_eqvt in eqvts makes this simpset always looping)
authorChristian Urban <urbanc@in.tum.de>
Thu, 04 Feb 2010 17:39:04 +0100
changeset 1063 b93b631570ca
parent 1062 dfea9e739231
child 1064 0391abfc6246
child 1066 96651cddeba9
fixed (permute_eqvt in eqvts makes this simpset always looping)
Quot/Nominal/Abs.thy file | annotate | diff | comparison | revisions 
--- a/Quot/Nominal/Abs.thy	Thu Feb 04 15:19:24 2010 +0100
+++ b/Quot/Nominal/Abs.thy	Thu Feb 04 17:39:04 2010 +0100
@@ -29,7 +29,7 @@
 apply(auto)
 apply(drule_tac x="p \<bullet> xa" in bspec)
 apply(unfold mem_def permute_fun_def)[1] 
-apply(simp add: eqvts)
+apply(simp add: eqvts del: permute_eqvt)
 apply(simp add: fresh_permute_iff)
 apply(rule_tac ?p1="- p" in fresh_permute_iff[THEN iffD1])
 apply(simp)
nominal2