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_Abs.thy
changeset 2663 54aade5d0fe6
parent 2659 619ecb57db38
child 2668 92c001d93225 
--- a/Nominal/Nominal2_Abs.thy	Mon Jan 17 12:33:37 2011 +0000
+++ b/Nominal/Nominal2_Abs.thy	Mon Jan 17 12:34:11 2011 +0000
@@ -444,7 +444,7 @@
 termination supp_lst 
   by (auto intro!: local.termination)
 
-lemma [eqvt]:
+lemma supp_funs_eqvt[eqvt]:
   shows "(p \<bullet> supp_set x) = supp_set (p \<bullet> x)"
   and   "(p \<bullet> supp_res y) = supp_res (p \<bullet> y)"
   and   "(p \<bullet> supp_lst z) = supp_lst (p \<bullet> z)"
@@ -461,7 +461,7 @@
   and   "a \<sharp> Abs_res bs x \<Longrightarrow> a \<sharp> supp_res (Abs_res bs x)"
   and   "a \<sharp> Abs_lst cs x \<Longrightarrow> a \<sharp> supp_lst (Abs_lst cs x)"
   by (rule_tac [!] fresh_fun_eqvt_app)
-     (simp_all only: eqvts_raw)
+     (auto simp only: eqvt_def eqvts_raw)
 
 lemma Abs_supp_subset1:
   assumes a: "finite (supp x)"
nominal2