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.
added let-eqvt back
authorChristian Urban <urbanc@in.tum.de>
Thu, 31 May 2012 11:59:56 +0100
changeset 3180 7b5db6c23753
parent 3178 a331468b2f5a
child 3181 ca162f0a7957
added let-eqvt back
Nominal/Nominal2_Base.thy file | annotate | diff | comparison | revisions
Nominal/Nominal2_Base_Exec.thy file | annotate | diff | comparison | revisions 
--- a/Nominal/Nominal2_Base.thy	Thu May 31 10:05:19 2012 +0100
+++ b/Nominal/Nominal2_Base.thy	Thu May 31 11:59:56 2012 +0100
@@ -876,6 +876,10 @@
   shows "p \<bullet> (if b then x else y) = (if p \<bullet> b then p \<bullet> x else p \<bullet> y)"
   by (simp add: permute_fun_def permute_bool_def)
 
+lemma Let_eqvt [eqvt]:
+  shows "p \<bullet> Let x y = Let (p \<bullet> x) (p \<bullet> y)"
+  unfolding Let_def permute_fun_app_eq ..
+
 lemma True_eqvt [eqvt]:
   shows "p \<bullet> True = True"
   unfolding permute_bool_def ..
--- a/Nominal/Nominal2_Base_Exec.thy	Thu May 31 10:05:19 2012 +0100
+++ b/Nominal/Nominal2_Base_Exec.thy	Thu May 31 11:59:56 2012 +0100
@@ -796,6 +796,10 @@
   shows "p \<bullet> (if b then x else y) = (if p \<bullet> b then p \<bullet> x else p \<bullet> y)"
   by (simp add: permute_fun_def permute_bool_def)
 
+lemma Let_eqvt [eqvt]:
+  shows "p \<bullet> Let x y = Let (p \<bullet> x) (p \<bullet> y)"
+  unfolding Let_def permute_fun_app_eq ..
+
 lemma True_eqvt [eqvt]:
   shows "p \<bullet> True = True"
   unfolding permute_bool_def ..
nominal2