# 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 +