src/Sequents/LK0.thy

--- 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