Mercurial Mercurial > hg > nominal2 / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal/Ex/Sigma.thy
author Christian Urban <urbanc@in.tum.de>
Mon, 09 Jan 2012 10:45:12 +0000 (2012-01-09)
changeset 3107 e26e933efba0
parent 3084 faeac3ae43e5
permissions -rw-r--r--
merged
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
nominal2