--- a/Nominal/Ex/ExPS6.thy	Wed Aug 25 23:16:42 2010 +0800
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,41 +0,0 @@
-theory ExPS6
-imports "../NewParser"
-begin
-
-(* example 6 from Peter Sewell's bestiary *)
-
-atom_decl name
-
-(* Is this binding structure supported - I think not 
-   because e1 occurs twice as body *)
-
-nominal_datatype exp =
-  Var name
-| Pair exp exp
-| LetRec x::name p::pat e1::exp e2::exp  bind x in e1 e2, bind "bp p" in e1
-and pat =
-  PVar name
-| PUnit
-| PPair pat pat
-binder
-  bp :: "pat \<Rightarrow> atom list"
-where
-  "bp (PVar x) = [atom x]"
-| "bp (PUnit) = []"
-| "bp (PPair p1 p2) = bp p1 @ bp p2"
-
-thm exp_pat.fv
-thm exp_pat.eq_iff
-thm exp_pat.bn
-thm exp_pat.perm
-thm exp_pat.induct
-thm exp_pat.distinct
-thm exp_pat.supp
-
-
-
-
-end
-
-
-