src/HOL/Nominal/Examples/Lambda_mu.thy
author wenzelm
Wed, 04 Oct 2017 12:00:53 +0200
changeset 66787 64b47495676d
parent 66453 cc19f7ca2ed6
child 80914 d97fdabd9e2b
permissions -rw-r--r--
obsolete;

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