author | wenzelm |
Mon, 11 Sep 2023 19:30:48 +0200 | |
changeset 78659 | b5f3d1051b13 |
parent 66453 | cc19f7ca2ed6 |
child 80914 | d97fdabd9e2b |
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