| author | Christian Urban <urbanc@in.tum.de> |
| Sat, 17 Dec 2011 16:36:51 +0000 | |
| branch | Nominal2-Isabelle2011-1 |
| changeset 3067 | c32bdb3f0a68 |
| parent 2686 | 52e1e98edb34 |
| child 3132 | 87eca760dcba |
| permissions | -rw-r--r-- |
theory Minimal imports "Nominal2" begin atom_decl name nominal_datatype lam = Var "name" | 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) end