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/Abs.thy
changeset 1675 d24f59f78a86
parent 1673 e8cf0520c820
child 1688 0b2535a72fd0 
--- a/Nominal/Abs.thy	Sat Mar 27 09:15:09 2010 +0100
+++ b/Nominal/Abs.thy	Sat Mar 27 09:21:43 2010 +0100
@@ -447,8 +447,9 @@
 
 lemma Abs_eq_iff:
   shows "Abs bs x = Abs cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op =) supp p (cs, y))"
-  by (lifting alpha_abs.simps(1))
-
+  and   "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op =) supp p (cs, y))"
+  and   "Abs_lst bsl x = Abs_lst csl y \<longleftrightarrow> (\<exists>p. (bsl, x) \<approx>lst (op =) supp p (csl, y))"
+  by (lifting alphas_abs)
 
 lemma split_rsp2[quot_respect]: "((R1 ===> R2 ===> prod_rel R1 R2 ===> op =) ===>
   prod_rel R1 R2 ===> prod_rel R1 R2 ===> op =) split split"
nominal2