--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Tutorial/Minimal.thy	Wed Jan 19 17:11:10 2011 +0100
@@ -0,0 +1,16 @@
+theory Minimal
+imports "../Nominal/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
\ No newline at end of file