observe standard convention for syntax consts;
authorwenzelm
Wed Feb 24 22:04:10 2010 +0100 (2010-02-24)
changeset 353542e8dc3c64430
parent 35353 1391f82da5a4
child 35355 613e133966ea
observe standard convention for syntax consts;
src/HOL/TLA/Action.thy
src/HOL/TLA/Intensional.thy
src/HOL/TLA/Stfun.thy
     1.1 --- a/src/HOL/TLA/Action.thy	Wed Feb 24 21:59:21 2010 +0100
     1.2 +++ b/src/HOL/TLA/Action.thy	Wed Feb 24 22:04:10 2010 +0100
     1.3 @@ -33,7 +33,7 @@
     1.4  
     1.5  syntax
     1.6    (* Syntax for writing action expressions in arbitrary contexts *)
     1.7 -  "ACT"         :: "lift => 'a"                      ("(ACT _)")
     1.8 +  "_ACT"        :: "lift => 'a"                      ("(ACT _)")
     1.9  
    1.10    "_before"     :: "lift => lift"                    ("($_)"  [100] 99)
    1.11    "_after"      :: "lift => lift"                    ("(_$)"  [100] 99)
     2.1 --- a/src/HOL/TLA/Intensional.thy	Wed Feb 24 21:59:21 2010 +0100
     2.2 +++ b/src/HOL/TLA/Intensional.thy	Wed Feb 24 22:04:10 2010 +0100
     2.3 @@ -51,7 +51,7 @@
     2.4    "_holdsAt"    :: "['a, lift] => bool"                  ("(_ |= _)" [100,10] 10)
     2.5  
     2.6    (* Syntax for lifted expressions outside the scope of |- or |= *)
     2.7 -  "LIFT"        :: "lift => 'a"                          ("LIFT _")
     2.8 +  "_LIFT"       :: "lift => 'a"                          ("LIFT _")
     2.9  
    2.10    (* generic syntax for lifted constants and functions *)
    2.11    "_const"      :: "'a => lift"                          ("(#_)" [1000] 999)
     3.1 --- a/src/HOL/TLA/Stfun.thy	Wed Feb 24 21:59:21 2010 +0100
     3.2 +++ b/src/HOL/TLA/Stfun.thy	Wed Feb 24 22:04:10 2010 +0100
     3.3 @@ -35,7 +35,7 @@
     3.4    stvars    :: "'a stfun => bool"
     3.5  
     3.6  syntax
     3.7 -  "PRED"    :: "lift => 'a"                          ("PRED _")
     3.8 +  "_PRED"   :: "lift => 'a"                          ("PRED _")
     3.9    "_stvars" :: "lift => bool"                        ("basevars _")
    3.10  
    3.11  translations