--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/SystemFOmega.thy	Wed Nov 24 02:36:21 2010 +0000
@@ -0,0 +1,51 @@
+theory SystemFOmega
+imports "../Nominal2"
+begin
+
+text {*
+  System from the F-ing paper by Rossberg, Russo and 
+  Dreyer, TLDI'10
+*}
+
+
+atom_decl var
+atom_decl tvar
+atom_decl label
+
+nominal_datatype kind =
+  \<Omega> | KFun kind kind
+
+nominal_datatype ty =
+  TVar tvar
+| TFun ty ty
+| TAll a::tvar kind t::ty bind a in t
+| TEx  a::tvar kind t::ty bind a in t
+| TLam a::tvar kind t::ty bind a in t
+| TApp ty ty
+| TRec trec
+and trec =
+  TRNil
+| TRCons label ty trec 
+
+nominal_datatype trm =
+  Var var
+| Lam x::var ty t::trm bind x in t
+| App trm trm
+| Dot trm label
+| LAM a::tvar kind t::trm bind a in t
+| APP trm ty
+| Pack ty trm
+| Unpack a::tvar x::var trm t::trm bind a x in t
+| Rec rec 
+and rec =
+  RNil
+| RCons label trm rec
+
+
+
+
+end
+
+
+
+

--- a/Nominal/ROOT.ML	Wed Nov 24 01:08:48 2010 +0000
+++ b/Nominal/ROOT.ML	Wed Nov 24 02:36:21 2010 +0000
@@ -19,6 +19,7 @@
     "Ex/Modules",
     "Ex/SingleLet",
     "Ex/Shallow",
+    "Ex/SystemFOmega",
     "Ex/TypeSchemes",
     "Ex/TypeVarsTest",
     "Ex/Foo1",