--- a/src/Sequents/LK0.thy Fri Nov 24 22:05:19 2006 +0100
+++ b/src/Sequents/LK0.thy Sun Nov 26 18:07:16 2006 +0100
@@ -20,7 +20,7 @@
consts
- Trueprop :: "two_seqi"
+ Trueprop :: "two_seqi"
True :: o
False :: o
@@ -50,18 +50,16 @@
"op |" :: "[o, o] => o" (infixr "\<or>" 30)
"op -->" :: "[o, o] => o" (infixr "\<longrightarrow>" 25)
"op <->" :: "[o, o] => o" (infixr "\<longleftrightarrow>" 25)
- "ALL " :: "[idts, o] => o" ("(3\<forall>_./ _)" [0, 10] 10)
- "EX " :: "[idts, o] => o" ("(3\<exists>_./ _)" [0, 10] 10)
- "EX! " :: "[idts, o] => o" ("(3\<exists>!_./ _)" [0, 10] 10)
+ All_binder :: "[idts, o] => o" ("(3\<forall>_./ _)" [0, 10] 10)
+ Ex_binder :: "[idts, o] => o" ("(3\<exists>_./ _)" [0, 10] 10)
"_not_equal" :: "['a, 'a] => o" (infixl "\<noteq>" 50)
syntax (HTML output)
Not :: "o => o" ("\<not> _" [40] 40)
"op &" :: "[o, o] => o" (infixr "\<and>" 35)
"op |" :: "[o, o] => o" (infixr "\<or>" 30)
- "ALL " :: "[idts, o] => o" ("(3\<forall>_./ _)" [0, 10] 10)
- "EX " :: "[idts, o] => o" ("(3\<exists>_./ _)" [0, 10] 10)
- "EX! " :: "[idts, o] => o" ("(3\<exists>!_./ _)" [0, 10] 10)
+ All_binder :: "[idts, o] => o" ("(3\<forall>_./ _)" [0, 10] 10)
+ Ex_binder :: "[idts, o] => o" ("(3\<exists>_./ _)" [0, 10] 10)
"_not_equal" :: "['a, 'a] => o" (infixl "\<noteq>" 50)
local