src/Sequents/LK0.thy
changeset 35113 1a0c129bb2e0
parent 30549 d2d7874648bd
child 35355 613e133966ea
child 35416 d8d7d1b785af
--- a/src/Sequents/LK0.thy	Thu Feb 11 22:06:37 2010 +0100
+++ b/src/Sequents/LK0.thy	Thu Feb 11 22:19:58 2010 +0100
@@ -1,10 +1,9 @@
 (*  Title:      LK/LK0.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
 There may be printing problems if a seqent is in expanded normal form
-        (eta-expanded, beta-contracted)
+(eta-expanded, beta-contracted).
 *)
 
 header {* Classical First-Order Sequent Calculus *}
@@ -35,10 +34,10 @@
   Ex           :: "('a => o) => o"   (binder "EX " 10)
 
 syntax
- "@Trueprop"    :: "two_seqe" ("((_)/ |- (_))" [6,6] 5)
+ "_Trueprop"    :: "two_seqe" ("((_)/ |- (_))" [6,6] 5)
 
-parse_translation {* [("@Trueprop", two_seq_tr "Trueprop")] *}
-print_translation {* [("Trueprop", two_seq_tr' "@Trueprop")] *}
+parse_translation {* [(@{syntax_const "_Trueprop"}, two_seq_tr @{const_syntax Trueprop})] *}
+print_translation {* [(@{const_syntax Trueprop}, two_seq_tr' @{syntax_const "_Trueprop"})] *}
 
 abbreviation
   not_equal  (infixl "~=" 50) where