# HG changeset patch # User Christian Urban # Date 1338461996 -3600 # Node ID 7b5db6c237535e8b38e267cc19d4f48bd7fba5a4 # Parent a331468b2f5a0af776de9491dc95e38fa333fdd2 added let-eqvt back diff -r a331468b2f5a -r 7b5db6c23753 Nominal/Nominal2_Base.thy --- 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 \ (if b then x else y) = (if p \ b then p \ x else p \ y)" by (simp add: permute_fun_def permute_bool_def) +lemma Let_eqvt [eqvt]: + shows "p \ Let x y = Let (p \ x) (p \ y)" + unfolding Let_def permute_fun_app_eq .. + lemma True_eqvt [eqvt]: shows "p \ True = True" unfolding permute_bool_def .. diff -r a331468b2f5a -r 7b5db6c23753 Nominal/Nominal2_Base_Exec.thy --- 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 \ (if b then x else y) = (if p \ b then p \ x else p \ y)" by (simp add: permute_fun_def permute_bool_def) +lemma Let_eqvt [eqvt]: + shows "p \ Let x y = Let (p \ x) (p \ y)" + unfolding Let_def permute_fun_app_eq .. + lemma True_eqvt [eqvt]: shows "p \ True = True" unfolding permute_bool_def ..