144 "w |= u = v" <= "_liftEqu u v w" |
144 "w |= u = v" <= "_liftEqu u v w" |
145 "w |= ALL x. A" <= "_RAll x A w" |
145 "w |= ALL x. A" <= "_RAll x A w" |
146 "w |= EX x. A" <= "_REx x A w" |
146 "w |= EX x. A" <= "_REx x A w" |
147 "w |= EX! x. A" <= "_REx1 x A w" |
147 "w |= EX! x. A" <= "_REx1 x A w" |
148 |
148 |
149 syntax (symbols) |
149 syntax (xsymbols) |
150 "_Valid" :: lift => bool ("(\\<turnstile> _)" 5) |
150 "_Valid" :: lift => bool ("(\\<turnstile> _)" 5) |
151 "_holdsAt" :: ['a, lift] => bool ("(_ \\<Turnstile> _)" [100,10] 10) |
151 "_holdsAt" :: ['a, lift] => bool ("(_ \\<Turnstile> _)" [100,10] 10) |
152 "_liftNeq" :: [lift, lift] => lift (infixl "\\<noteq>" 50) |
152 "_liftNeq" :: [lift, lift] => lift (infixl "\\<noteq>" 50) |
153 "_liftNot" :: lift => lift ("\\<not> _" [40] 40) |
153 "_liftNot" :: lift => lift ("\\<not> _" [40] 40) |
154 "_liftAnd" :: [lift, lift] => lift (infixr "\\<and>" 35) |
154 "_liftAnd" :: [lift, lift] => lift (infixr "\\<and>" 35) |
155 "_liftOr" :: [lift, lift] => lift (infixr "\\<or>" 30) |
155 "_liftOr" :: [lift, lift] => lift (infixr "\\<or>" 30) |
156 "_liftImp" :: [lift, lift] => lift (infixr "\\<midarrow>\\<rightarrow>" 25) |
156 "_liftImp" :: [lift, lift] => lift (infixr "\\<longrightarrow>" 25) |
157 "_RAll" :: [idts, lift] => lift ("(3\\<forall>_./ _)" [0, 10] 10) |
157 "_RAll" :: [idts, lift] => lift ("(3\\<forall>_./ _)" [0, 10] 10) |
158 "_REx" :: [idts, lift] => lift ("(3\\<exists>_./ _)" [0, 10] 10) |
158 "_REx" :: [idts, lift] => lift ("(3\\<exists>_./ _)" [0, 10] 10) |
159 "_REx1" :: [idts, lift] => lift ("(3\\<exists>!_./ _)" [0, 10] 10) |
159 "_REx1" :: [idts, lift] => lift ("(3\\<exists>!_./ _)" [0, 10] 10) |
160 "_liftLeq" :: [lift, lift] => lift ("(_/ \\<le> _)" [50, 51] 50) |
160 "_liftLeq" :: [lift, lift] => lift ("(_/ \\<le> _)" [50, 51] 50) |
161 "_liftMem" :: [lift, lift] => lift ("(_/ \\<in> _)" [50, 51] 50) |
161 "_liftMem" :: [lift, lift] => lift ("(_/ \\<in> _)" [50, 51] 50) |