author | wenzelm |
Wed, 04 Oct 2017 12:00:53 +0200 | |
changeset 66787 | 64b47495676d |
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