# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1324372068 -32400
# Node ID faeac3ae43e5cadc565d7db4b1cc725bb35215a0
# Parent  16b5f41890758419ca4f5b00ece8103e0ec19cb8
Add Sigma.thy, an example that defines a sigma-calculus in the style of Peter Homeier's HOL4 formalization.

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
+