diff -r 16b5f4189075 -r faeac3ae43e5 Nominal/Ex/Sigma.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/Sigma.thy	Tue Dec 20 18:07:48 2011 +0900
@@ -0,0 +1,20 @@
+theory Sigma
+imports Nominal2
+begin
+
+atom_decl name
+
+nominal_datatype obj =
+  Var name
+| Obj smlst
+| Inv obj string
+| Upd obj string method
+and smlst =
+  SMNil
+| SMCons string method smlst
+and method =
+  Sig n::name o::obj binds n in o
+
+
+end
+