--- a/src/HOL/TLA/TLA.thy Wed Feb 10 00:45:16 2010 +0100
+++ b/src/HOL/TLA/TLA.thy Wed Feb 10 00:46:56 2010 +0100
@@ -37,12 +37,12 @@
"_AAll" :: "[idts, lift] => lift" ("(3AALL _./ _)" [0,10] 10)
translations
- "_Box" == "Box"
- "_Dmd" == "Dmd"
- "_leadsto" == "leadsto"
- "_stable" == "Stable"
- "_WF" == "WF"
- "_SF" == "SF"
+ "_Box" == "CONST Box"
+ "_Dmd" == "CONST Dmd"
+ "_leadsto" == "CONST leadsto"
+ "_stable" == "CONST Stable"
+ "_WF" == "CONST WF"
+ "_SF" == "CONST SF"
"_EEx v A" == "Eex v. A"
"_AAll v A" == "Aall v. A"