| author | Christian Urban <christian dot urban at kcl dot ac dot uk> |
| Tue, 19 Feb 2013 05:38:46 +0000 | |
| branch | Nominal2-Isabelle2013 |
| changeset 3206 | fb201e383f1b |
| parent 3132 | 87eca760dcba |
| child 3235 | 5ebd327ffb96 |
| 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" binds 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