diff -r c50601bc617e -r 72cdd2af7eb4 Nominal/Ex/Ex1.thy
--- a/Nominal/Ex/Ex1.thy	Wed Apr 21 10:13:17 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,36 +0,0 @@
-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
-
-
-