1theory Lambda_mu 2 imports "HOL-Nominal.Nominal" 3begin 4 5section \<open>Lambda-Mu according to a paper by Gavin Bierman\<close> 6 7atom_decl var mvar 8 9nominal_datatype trm = 10 Var "var" 11 | Lam "\<guillemotleft>var\<guillemotright>trm" ("Lam [_]._" [100,100] 100) 12 | App "trm" "trm" 13 | Pss "mvar" "trm" (* passivate *) 14 | Act "\<guillemotleft>mvar\<guillemotright>trm" ("Act [_]._" [100,100] 100) (* activate *) 15 16 17end 18