diff -r 1df873b63cb2 -r 52e1e98edb34 Tutorial/Minimal.thy --- a/Tutorial/Minimal.thy Wed Jan 19 19:41:50 2011 +0100 +++ b/Tutorial/Minimal.thy Wed Jan 19 23:58:12 2011 +0100 @@ -9,6 +9,8 @@ | App "lam" "lam" | Lam x::"name" l::"lam" bind x in l ("Lam [_]. _" [100, 100] 100) + + lemma alpha_test: shows "Lam [x]. (Var x) = Lam [y]. (Var y)" by (simp add: lam.eq_iff Abs1_eq_iff lam.fresh fresh_at_base)