author | wenzelm |
Fri, 18 Aug 2017 20:47:47 +0200 | |
changeset 66453 | cc19f7ca2ed6 |
parent 63167 | 0909deb8059b |
permissions | -rw-r--r-- |
theory Lambda_mu imports "HOL-Nominal.Nominal" begin section \<open>Lambda-Mu according to a paper by Gavin Bierman\<close> 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