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