--- a/src/HOL/Nominal/Examples/Lambda_mu.thy Tue Jan 08 11:37:37 2008 +0100
+++ b/src/HOL/Nominal/Examples/Lambda_mu.thy Tue Jan 08 23:11:08 2008 +0100
@@ -1,7 +1,7 @@
(* $Id$ *)
theory Lambda_mu
-imports "../Nominal"
+ imports "../Nominal"
begin
section {* Lambda-Mu according to a paper by Gavin Bierman *}
@@ -12,7 +12,8 @@
Var "var"
| Lam "\<guillemotleft>var\<guillemotright>trm" ("Lam [_]._" [100,100] 100)
| App "trm" "trm"
- | Pss "mvar" "trm"
- | Act "\<guillemotleft>mvar\<guillemotright>trm" ("Act [_]._" [100,100] 100)
+ | Pss "mvar" "trm" (* passivate *)
+ | Act "\<guillemotleft>mvar\<guillemotright>trm" ("Act [_]._" [100,100] 100) (* activate *)
+
end