# HG changeset patch # User Cezary Kaliszyk # Date 1307599438 -32400 # Node ID 177a32a4f289945e311f48f060ca84731132cd81 # Parent bcf48a1cb24b01b807172b2cdd0810a536c2fa2d Minor simplification diff -r bcf48a1cb24b -r 177a32a4f289 Nominal/Ex/Lambda.thy --- a/Nominal/Ex/Lambda.thy Thu Jun 09 11:10:41 2011 +0900 +++ b/Nominal/Ex/Lambda.thy Thu Jun 09 15:03:58 2011 +0900 @@ -273,7 +273,7 @@ apply(subgoal_tac "(atom x \ atom xa) \ sa = sa") apply(subgoal_tac "(atom x \ atom xa) \ ya = ya") apply(simp add: eqvt_at_def) -apply(rule perm_supp_eq,simp add: fresh_star_def fresh_Pair supp_swap)+ +apply(simp_all add: swap_fresh_fresh) done termination