diff -r 263aaf988d44 -r c24395ea4e71 src/HOL/Nominal/Examples/Lambda_mu.thy
--- 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