author | blanchet |
Tue, 16 Sep 2014 19:23:37 +0200 | |
changeset 58352 | 37745650a3f4 |
parent 41589 | bbd861837ebc |
child 63167 | 0909deb8059b |
permissions | -rw-r--r-- |
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