# HG changeset patch
# User wenzelm
# Date 1267045450 -3600
# Node ID 2e8dc3c6443015e6b782ccc797d0a668b265711a
# Parent  1391f82da5a4c391443e433eedf2414ef52f7d0e
observe standard convention for syntax consts;

diff -r 1391f82da5a4 -r 2e8dc3c64430 src/HOL/TLA/Action.thy
--- a/src/HOL/TLA/Action.thy	Wed Feb 24 21:59:21 2010 +0100
+++ b/src/HOL/TLA/Action.thy	Wed Feb 24 22:04:10 2010 +0100
@@ -33,7 +33,7 @@
 
 syntax
   (* Syntax for writing action expressions in arbitrary contexts *)
-  "ACT"         :: "lift => 'a"                      ("(ACT _)")
+  "_ACT"        :: "lift => 'a"                      ("(ACT _)")
 
   "_before"     :: "lift => lift"                    ("($_)"  [100] 99)
   "_after"      :: "lift => lift"                    ("(_$)"  [100] 99)
diff -r 1391f82da5a4 -r 2e8dc3c64430 src/HOL/TLA/Intensional.thy
--- a/src/HOL/TLA/Intensional.thy	Wed Feb 24 21:59:21 2010 +0100
+++ b/src/HOL/TLA/Intensional.thy	Wed Feb 24 22:04:10 2010 +0100
@@ -51,7 +51,7 @@
   "_holdsAt"    :: "['a, lift] => bool"                  ("(_ |= _)" [100,10] 10)
 
   (* Syntax for lifted expressions outside the scope of |- or |= *)
-  "LIFT"        :: "lift => 'a"                          ("LIFT _")
+  "_LIFT"       :: "lift => 'a"                          ("LIFT _")
 
   (* generic syntax for lifted constants and functions *)
   "_const"      :: "'a => lift"                          ("(#_)" [1000] 999)
diff -r 1391f82da5a4 -r 2e8dc3c64430 src/HOL/TLA/Stfun.thy
--- a/src/HOL/TLA/Stfun.thy	Wed Feb 24 21:59:21 2010 +0100
+++ b/src/HOL/TLA/Stfun.thy	Wed Feb 24 22:04:10 2010 +0100
@@ -35,7 +35,7 @@
   stvars    :: "'a stfun => bool"
 
 syntax
-  "PRED"    :: "lift => 'a"                          ("PRED _")
+  "_PRED"   :: "lift => 'a"                          ("PRED _")
   "_stvars" :: "lift => bool"                        ("basevars _")
 
 translations