diff -r 5335c0ea743a -r 313e6f2cdd89 Tutorial/Lambda.thy --- a/Tutorial/Lambda.thy Thu May 31 12:01:13 2012 +0100 +++ b/Tutorial/Lambda.thy Mon Jun 04 21:39:51 2012 +0100 @@ -39,7 +39,6 @@ | "height (App t1 t2) = max (height t1) (height t2) + 1" | "height (Lam [x].t) = height t + 1" apply(simp add: eqvt_def height_graph_def) -apply (rule, perm_simp, rule) apply(rule TrueI) apply(rule_tac y="x" in lam.exhaust) apply(auto) @@ -69,8 +68,10 @@ apply(erule_tac c="(ya,sa)" in Abs_lst1_fcb2) apply(simp_all add: Abs_fresh_iff) apply(simp add: fresh_star_def fresh_Pair) - apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) - apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) + apply(simp add: eqvt_at_def) + apply(simp add: perm_supp_eq fresh_star_Pair) + apply(simp add: eqvt_at_def) + apply(simp add: perm_supp_eq fresh_star_Pair) done termination (eqvt) @@ -82,7 +83,7 @@ shows "atom z \ t[y ::= s]" using a b by (nominal_induct t avoiding: z y s rule: lam.strong_induct) - (auto simp add: lam.fresh fresh_at_base) + (auto simp add: fresh_at_base) end