--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/CoreHaskell2.thy	Wed Dec 22 09:13:25 2010 +0000
@@ -0,0 +1,79 @@
+theory CoreHaskell2
+imports "../Nominal2"
+begin
+
+(* Core Haskell by John Matthews *)
+
+atom_decl var
+atom_decl cvar
+atom_decl tvar
+
+
+nominal_datatype kinds:
+    Kind =
+       Klifted
+     | Kunlifted
+     | Kopen
+     | Karrow Kind Kind
+     | Keq Ty Ty
+and Ty =
+       Tvar tvar
+     | Tcon string
+     | Tapp Ty Ty
+     | Tforall pb::PBind ty::Ty   bind "bind_pb pb" in ty
+and PBind =
+  Pbind tvar Kind
+binder
+  bind_pb
+where
+  "bind_pb (Pbind tv k) = [atom tv]"
+
+nominal_datatype expressions:
+    Bind =
+       Vb var Ty
+     | Tb tvar Kind
+and Exp =
+       Var var
+     | Dcon string
+     | App Exp Exp
+     | Appt Exp Ty
+     | Lam b::Bind e::Exp bind "bind_b b" in e
+binder
+  bind_b
+where
+  "bind_b (Vb v ty) = [atom v]"
+| "bind_b (Tb tv kind) = [atom tv]"
+
+thm kinds.distinct
+thm kinds.induct
+thm kinds.inducts
+thm kinds.exhaust
+thm kinds.strong_exhaust
+thm kinds.fv_defs
+thm kinds.bn_defs
+thm kinds.perm_simps
+thm kinds.eq_iff
+thm kinds.fv_bn_eqvt
+thm kinds.size_eqvt
+thm kinds.supports
+thm kinds.fsupp
+thm kinds.supp
+thm kinds.fresh
+
+thm expressions.distinct
+thm expressions.induct
+thm expressions.inducts
+thm expressions.exhaust
+thm expressions.fv_defs
+thm expressions.bn_defs
+thm expressions.perm_simps
+thm expressions.eq_iff
+thm expressions.fv_bn_eqvt
+thm expressions.size_eqvt
+thm expressions.supports
+thm expressions.fsupp
+thm expressions.supp
+thm expressions.fresh
+
+end
+