changeset 14765 | bafb24c150c1 |
parent 14565 | c6dc17aab88a |
child 14854 | 61bdf2ae4dc5 |
--- a/src/Sequents/LK0.thy Wed May 19 11:41:58 2004 +0200 +++ b/src/Sequents/LK0.thy Fri May 21 21:14:18 2004 +0200 @@ -22,7 +22,6 @@ consts Trueprop :: "two_seqi" - "@Trueprop" :: "two_seqe" ("((_)/ |- (_))" [6,6] 5) True,False :: o "=" :: ['a,'a] => o (infixl 50) @@ -35,6 +34,7 @@ Ex :: ('a => o) => o (binder "EX " 10) syntax + "@Trueprop" :: "two_seqe" ("((_)/ |- (_))" [6,6] 5) "_not_equal" :: ['a, 'a] => o (infixl "~=" 50) translations