--- a/src/Sequents/ILL.thy Wed May 09 19:37:18 2007 +0200
+++ b/src/Sequents/ILL.thy Wed May 09 19:37:19 2007 +0200
@@ -11,16 +11,16 @@
consts
Trueprop :: "two_seqi"
-"><" ::"[o, o] => o" (infixr 35)
-"-o" ::"[o, o] => o" (infixr 45)
-"o-o" ::"[o, o] => o" (infixr 45)
-FShriek ::"o => o" ("! _" [100] 1000)
-"&&" ::"[o, o] => o" (infixr 35)
-"++" ::"[o, o] => o" (infixr 35)
-zero ::"o" ("0")
-top ::"o" ("1")
-eye ::"o" ("I")
-aneg ::"o=>o" ("~_")
+ tens :: "[o, o] => o" (infixr "><" 35)
+ limp :: "[o, o] => o" (infixr "-o" 45)
+ liff :: "[o, o] => o" (infixr "o-o" 45)
+ FShriek :: "o => o" ("! _" [100] 1000)
+ lconj :: "[o, o] => o" (infixr "&&" 35)
+ ldisj :: "[o, o] => o" (infixr "++" 35)
+ zero :: "o" ("0")
+ top :: "o" ("1")
+ eye :: "o" ("I")
+ aneg :: "o=>o" ("~_")
(* context manipulation *)
--- a/src/Sequents/LK0.thy Wed May 09 19:37:18 2007 +0200
+++ b/src/Sequents/LK0.thy Wed May 09 19:37:19 2007 +0200
@@ -24,43 +24,43 @@
True :: o
False :: o
- "=" :: "['a,'a] => o" (infixl 50)
+ equal :: "['a,'a] => o" (infixl "=" 50)
Not :: "o => o" ("~ _" [40] 40)
- "&" :: "[o,o] => o" (infixr 35)
- "|" :: "[o,o] => o" (infixr 30)
- "-->" :: "[o,o] => o" (infixr 25)
- "<->" :: "[o,o] => o" (infixr 25)
+ conj :: "[o,o] => o" (infixr "&" 35)
+ disj :: "[o,o] => o" (infixr "|" 30)
+ imp :: "[o,o] => o" (infixr "-->" 25)
+ iff :: "[o,o] => o" (infixr "<->" 25)
The :: "('a => o) => 'a" (binder "THE " 10)
All :: "('a => o) => o" (binder "ALL " 10)
Ex :: "('a => o) => o" (binder "EX " 10)
syntax
"@Trueprop" :: "two_seqe" ("((_)/ |- (_))" [6,6] 5)
- "_not_equal" :: "['a, 'a] => o" (infixl "~=" 50)
parse_translation {* [("@Trueprop", two_seq_tr "Trueprop")] *}
print_translation {* [("Trueprop", two_seq_tr' "@Trueprop")] *}
-translations
- "x ~= y" == "~ (x = y)"
+abbreviation
+ not_equal (infixl "~=" 50) where
+ "x ~= y == ~ (x = y)"
syntax (xsymbols)
Not :: "o => o" ("\<not> _" [40] 40)
- "op &" :: "[o, o] => o" (infixr "\<and>" 35)
- "op |" :: "[o, o] => o" (infixr "\<or>" 30)
- "op -->" :: "[o, o] => o" (infixr "\<longrightarrow>" 25)
- "op <->" :: "[o, o] => o" (infixr "\<longleftrightarrow>" 25)
+ conj :: "[o, o] => o" (infixr "\<and>" 35)
+ disj :: "[o, o] => o" (infixr "\<or>" 30)
+ imp :: "[o, o] => o" (infixr "\<longrightarrow>" 25)
+ iff :: "[o, o] => o" (infixr "\<longleftrightarrow>" 25)
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)
+ 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)
+ conj :: "[o, o] => o" (infixr "\<and>" 35)
+ disj :: "[o, o] => o" (infixr "\<or>" 30)
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)
+ not_equal :: "['a, 'a] => o" (infixl "\<noteq>" 50)
local