changeset 2686 | 52e1e98edb34 |
parent 2681 | 0e4c5fa26fa1 |
child 3132 | 87eca760dcba |
--- 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)