author | urbanc |
Tue, 08 Jan 2008 23:11:08 +0100 | |
changeset 25867 | c24395ea4e71 |
parent 22829 | f1db55c7534d |
child 41589 | bbd861837ebc |
permissions | -rw-r--r-- |
(* $Id$ *) theory Lambda_mu imports "../Nominal" begin section {* Lambda-Mu according to a paper by Gavin Bierman *} atom_decl var mvar nominal_datatype trm = Var "var" | Lam "\<guillemotleft>var\<guillemotright>trm" ("Lam [_]._" [100,100] 100) | App "trm" "trm" | Pss "mvar" "trm" (* passivate *) | Act "\<guillemotleft>mvar\<guillemotright>trm" ("Act [_]._" [100,100] 100) (* activate *) end