--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex1.thy	Tue Mar 23 08:42:02 2010 +0100
@@ -0,0 +1,36 @@
+theory Ex1
+imports "Parser"
+begin
+
+text {* example 1, equivalent to example 2 from Terms *}
+
+atom_decl name
+
+ML {* val _ = recursive := false *}
+nominal_datatype lam =
+  VAR "name"
+| APP "lam" "lam"
+| LAM x::"name" t::"lam" bind x in t
+| LET bp::"bp" t::"lam"   bind "bi bp" in t
+and bp =
+  BP "name" "lam"
+binder
+  bi::"bp \<Rightarrow> atom set"
+where
+  "bi (BP x t) = {atom x}"
+
+thm lam_bp.fv
+thm lam_bp.supp
+thm lam_bp.eq_iff
+thm lam_bp.bn
+thm lam_bp.perm
+thm lam_bp.induct
+thm lam_bp.inducts
+thm lam_bp.distinct
+ML {* Sign.of_sort @{theory} (@{typ lam}, @{sort fs}) *}
+thm lam_bp.fv[simplified lam_bp.supp]
+
+end
+
+
+