src/HOL/TLA/Intensional.thy
changeset 35354 2e8dc3c64430
parent 35318 e1b61c5fd494
child 38549 d0385f2764d8
     1.1 --- a/src/HOL/TLA/Intensional.thy	Wed Feb 24 21:59:21 2010 +0100
     1.2 +++ b/src/HOL/TLA/Intensional.thy	Wed Feb 24 22:04:10 2010 +0100
     1.3 @@ -51,7 +51,7 @@
     1.4    "_holdsAt"    :: "['a, lift] => bool"                  ("(_ |= _)" [100,10] 10)
     1.5  
     1.6    (* Syntax for lifted expressions outside the scope of |- or |= *)
     1.7 -  "LIFT"        :: "lift => 'a"                          ("LIFT _")
     1.8 +  "_LIFT"       :: "lift => 'a"                          ("LIFT _")
     1.9  
    1.10    (* generic syntax for lifted constants and functions *)
    1.11    "_const"      :: "'a => lift"                          ("(#_)" [1000] 999)