# HG changeset patch # User Cezary Kaliszyk # Date 1269668656 -3600 # Node ID a99ae705b81115abf9df538a528ff5fb707053bc # Parent d00dd828f7affcf5d4d402338b85d2c8f9e450af Removed some warnings. diff -r d00dd828f7af -r a99ae705b811 Nominal/Abs.thy --- a/Nominal/Abs.thy Fri Mar 26 22:23:22 2010 +0100 +++ b/Nominal/Abs.thy Sat Mar 27 06:44:16 2010 +0100 @@ -54,22 +54,25 @@ fun alpha_abs where + [simp del]: "alpha_abs (bs, x) (cs, y) \ (\p. (bs, x) \gen (op=) supp p (cs, y))" fun alpha_abs_lst where + [simp del]: "alpha_abs_lst (bs, x) (cs, y) \ (\p. (bs, x) \lst (op=) supp p (cs, y))" fun alpha_abs_res where + [simp del]: "alpha_abs_res (bs, x) (cs, y) \ (\p. (bs, x) \res (op=) supp p (cs, y))" notation - alpha_abs ("_ \abs _") and - alpha_abs_lst ("_ \abs'_lst _") and - alpha_abs_res ("_ \abs'_res _") + alpha_abs (infix "\abs" 50) and + alpha_abs_lst (infix "\abs'_lst" 50) and + alpha_abs_res (infix "\abs'_res" 50) lemmas alphas_abs = alpha_abs.simps alpha_abs_res.simps alpha_abs_lst.simps @@ -208,7 +211,7 @@ shows "Abs bs x = Abs cs y \ (bs, x) \abs (cs, y)" and "Abs_res bs x = Abs_res cs y \ (bs, x) \abs_res (cs, y)" and "Abs_lst ds x = Abs_lst hs y \ (ds, x) \abs_lst (hs, y)" - apply(simp_all) + apply(simp_all add: alphas_abs) apply(lifting alphas_abs) done