--- 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)
--- 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)
--- 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