more complete simpset for linear arithmetic to avoid warnings: terms such as (2x + 2y)/2 can then be simplified by the linear arithmetic prover during its proof replay
theory Lambda_mu
imports "../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