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 1688 0b2535a72fd0
parent 1686 7b3dd407f6b3
parent 1675 d24f59f78a86
child 1691 b497ac81aead 
--- a/Nominal/Abs.thy	Mon Mar 29 00:30:20 2010 +0200
+++ b/Nominal/Abs.thy	Mon Mar 29 00:30:47 2010 +0200
@@ -419,8 +419,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