Nominal/Ex/Sigma.thy
author Christian Urban <urbanc@in.tum.de>
Tue, 24 Jan 2012 14:05:24 +0000
changeset 3110 62e1d888aacc
parent 3084 faeac3ae43e5
permissions -rw-r--r--
added a session entry in order to quickly build the heap file (tests took too long)

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