Mercurial Mercurial > repos > isabelle / 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.
src/HOL/Nominal/Nominal.thy
changeset 22774 8c64803fae48
parent 22768 d41fe3416f52
child 22775 d08efe73b27f 
--- a/src/HOL/Nominal/Nominal.thy	Mon Apr 23 20:44:12 2007 +0200
+++ b/src/HOL/Nominal/Nominal.thy	Tue Apr 24 14:01:23 2007 +0200
@@ -634,6 +634,11 @@
   shows "pi1 \<triangleq> pi2 \<Longrightarrow> (rev pi1) \<triangleq> (rev pi2)"
   by (simp add: at_prm_rev_eq[OF at])
 
+lemma at_perm_fresh_fresh:
+  fixes a  :: "'x"
+  assumes 
+
+
 lemma at_ds1:
   fixes a  :: "'x"
   assumes at: "at TYPE('x)"
isabelle