src/HOL/TLA/Intensional.thy
changeset 6340 7d5cbd5819a0
parent 6255 db63752140c7
child 7224 e41e64476f9b
     1.1 --- a/src/HOL/TLA/Intensional.thy	Wed Mar 10 10:53:53 1999 +0100
     1.2 +++ b/src/HOL/TLA/Intensional.thy	Wed Mar 10 10:55:12 1999 +0100
     1.3 @@ -161,6 +161,9 @@
     1.4    "_liftMem"    :: [lift, lift] => lift                ("(_/ \\<in> _)" [50, 51] 50)
     1.5    "_liftNotMem" :: [lift, lift] => lift                ("(_/ \\<notin> _)" [50, 51] 50)
     1.6  
     1.7 +syntax (HTML output)
     1.8 +  "_liftNot"    :: lift => lift                        ("\\<not> _" [40] 40)
     1.9 +
    1.10  rules
    1.11    Valid_def   "|- A    ==  ALL w. w |= A"
    1.12  
    1.13 @@ -173,5 +176,3 @@
    1.14    unl_Rex     "w |= ? x. A x  ==  ? x. (w |= A x)"
    1.15    unl_Rex1    "w |= ?! x. A x  ==  ?! x. (w |= A x)"
    1.16  end
    1.17 -
    1.18 -ML