Sara Kalvala: moving the <<...>> notation from LK to Sequents

--- a/src/Sequents/LK0.thy	Tue Aug 03 13:15:54 1999 +0200
+++ b/src/Sequents/LK0.thy	Tue Aug 03 13:16:29 1999 +0200
@@ -24,9 +24,6 @@
  Trueprop	:: "two_seqi"
  "@Trueprop"	:: "two_seqe" ("((_)/ |- (_))" [6,6] 5)
 
-  (*Constant to allow definitions of SEQUENCES of formulas*)
-  "@Side"        :: "seq=>(seq'=>seq')"     ("<<(_)>>")
-
   True,False   :: o
   "="          :: ['a,'a] => o       (infixl 50)
   Not          :: o => o             ("~ _" [40] 40)
@@ -138,9 +135,7 @@
 
 ML
 
-fun side_tr [s1] = Sequents.seq_tr s1;
 
-val parse_translation = [("@Trueprop",Sequents.two_seq_tr "Trueprop"),
-			 ("@Side", side_tr)];
+val parse_translation = [("@Trueprop",Sequents.two_seq_tr "Trueprop")];
 val print_translation = [("Trueprop",Sequents.two_seq_tr' "@Trueprop")];
 

--- a/src/Sequents/Sequents.thy	Tue Aug 03 13:15:54 1999 +0200
+++ b/src/Sequents/Sequents.thy	Tue Aug 03 13:16:29 1999 +0200
@@ -3,7 +3,8 @@
     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
-Classical First-Order Sequent Calculus
+Basis theory for parsing and pretty-printing of sequences to be used in
+Sequent Calculi. 
 *)
 
 Sequents = Pure +
@@ -23,8 +24,8 @@
  seq'
 
 consts
- SeqO'         :: "[o,seq']=>seq'"
- Seq1'         :: "o=>seq'"
+ SeqO'         :: [o,seq']=>seq'
+ Seq1'         :: o=>seq'
     
 
 (* concrete syntax *)
@@ -34,25 +35,33 @@
 
 
 syntax
- SeqEmp         :: "seq"                                ("")
- SeqApp         :: "[seqobj,seqcont] => seq"            ("__")
+ SeqEmp         :: seq                                ("")
+ SeqApp         :: [seqobj,seqcont] => seq            ("__")
 
- SeqContEmp     :: "seqcont"                            ("")
- SeqContApp     :: "[seqobj,seqcont] => seqcont"        (",/ __")
+ SeqContEmp     :: seqcont                            ("")
+ SeqContApp     :: [seqobj,seqcont] => seqcont        (",/ __")
   
- SeqO           :: "o => seqobj"                        ("_")
- SeqId          :: "'a => seqobj"                       ("$_")
+ SeqO           :: o => seqobj                        ("_")
+ SeqId          :: 'a => seqobj                       ("$_")
 
 types
     
- single_seqe = "[seq,seqobj] => prop"
- single_seqi = "[seq'=>seq',seq'=>seq'] => prop"
- two_seqi = "[seq'=>seq', seq'=>seq'] => prop"
- two_seqe = "[seq, seq] => prop"
- three_seqi = "[seq'=>seq', seq'=>seq', seq'=>seq'] => prop"
- three_seqe = "[seq, seq, seq] => prop"
- four_seqi = "[seq'=>seq', seq'=>seq', seq'=>seq', seq'=>seq'] => prop"
- four_seqe = "[seq, seq, seq, seq] => prop"
+ single_seqe = [seq,seqobj] => prop
+ single_seqi = [seq'=>seq',seq'=>seq'] => prop
+ two_seqi    = [seq'=>seq', seq'=>seq'] => prop
+ two_seqe    = [seq, seq] => prop
+ three_seqi  = [seq'=>seq', seq'=>seq', seq'=>seq'] => prop
+ three_seqe  = [seq, seq, seq] => prop
+ four_seqi   = [seq'=>seq', seq'=>seq', seq'=>seq', seq'=>seq'] => prop
+ four_seqe   = [seq, seq, seq, seq] => prop
+
+
+ sequence_name = seq'=>seq'
+
+
+consts
+  (*Constant to allow definitions of SEQUENCES of formulas*)
+  "@Side"        :: seq=>(seq'=>seq')     ("<<(_)>>")
 
 end
 
@@ -146,3 +155,8 @@
 
 
 			 
+(** for the <<...>> notation **)
+  
+fun side_tr [s1] = seq_tr s1;
+
+val parse_translation = [("@Side", side_tr)];