diff -r 6ac12b9478d5 -r fb0655539d05 src/Sequents/Sequents.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Sequents/Sequents.thy	Wed Oct 09 13:32:33 1996 +0200
@@ -0,0 +1,147 @@
+(*  Title: 	LK/lk.thy
+    ID:         $Id$
+    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1993  University of Cambridge
+
+Classical First-Order Sequent Calculus
+*)
+
+Sequents = Pure +
+
+types
+  o 
+
+arities
+  o :: logic
+
+
+(* Sequences *)
+
+types
+ seq'
+
+consts
+ SeqO'         :: "[o,seq']=>seq'"
+ Seq1'         :: "o=>seq'"
+    
+
+(* concrete syntax *)
+
+types
+  seq seqobj seqcont
+
+
+syntax
+ SeqEmp         :: "seq"                                ("")
+ SeqApp         :: "[seqobj,seqcont] => seq"            ("__")
+
+ SeqContEmp     :: "seqcont"                            ("")
+ SeqContApp     :: "[seqobj,seqcont] => seqcont"        (",/ __")
+  
+ SeqO           :: "o => seqobj"                        ("_")
+ SeqId          :: "id => seqobj"                       ("$_")
+ SeqVar         :: "var => 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"
+
+end
+
+ML
+
+(* parse translation for sequences *)
+
+fun abs_seq' t = Abs("s", Type("seq'",[]), t);
+
+fun seqobj_tr(Const("SeqO",_)$f) = Const("SeqO'",dummyT)$f |
+    seqobj_tr(_$i) = i;
+    
+fun seqcont_tr(Const("SeqContEmp",_)) = Bound 0 |
+    seqcont_tr(Const("SeqContApp",_)$so$sc) = 
+      (seqobj_tr so)$(seqcont_tr sc);
+
+fun seq_tr(Const("SeqEmp",_)) = abs_seq'(Bound 0) |
+    seq_tr(Const("SeqApp",_)$so$sc) = 
+      abs_seq'(seqobj_tr(so)$seqcont_tr(sc));
+
+
+fun singlobj_tr(Const("SeqO",_)$f) =
+    abs_seq' ((Const("SeqO'",dummyT)$f)$Bound 0);
+    
+
+    
+(* print translation for sequences *)
+
+fun seqcont_tr' (Bound 0) = 
+      Const("SeqContEmp",dummyT) |
+    seqcont_tr' (Const("SeqO'",_)$f$s) =
+      Const("SeqContApp",dummyT)$
+      (Const("SeqO",dummyT)$f)$
+      (seqcont_tr' s) |
+(*    seqcont_tr' ((a as Abs(_,_,_))$s)= 
+      seqcont_tr'(betapply(a,s)) | *)
+    seqcont_tr' (i$s) = 
+      Const("SeqContApp",dummyT)$
+      (Const("SeqId",dummyT)$i)$
+      (seqcont_tr' s);
+
+fun seq_tr' s =
+    let fun seq_itr' (Bound 0) = 
+              Const("SeqEmp",dummyT) |
+            seq_itr' (Const("SeqO'",_)$f$s) =
+              Const("SeqApp",dummyT)$
+              (Const("SeqO",dummyT)$f)$(seqcont_tr' s) |
+(*            seq_itr' ((a as Abs(_,_,_))$s) =
+              seq_itr'(betapply(a,s)) |    *)
+            seq_itr' (i$s) =
+              Const("SeqApp",dummyT)$
+              (Const("SeqId",dummyT)$i)$
+              (seqcont_tr' s)
+    in case s of 
+         Abs(_,_,t) => seq_itr' t |
+         _ => s$(Bound 0)
+    end;
+
+
+
+
+fun single_tr c [s1,s2] =
+    Const(c,dummyT)$seq_tr s1$singlobj_tr s2;
+
+fun two_seq_tr c [s1,s2] =
+    Const(c,dummyT)$seq_tr s1$seq_tr s2;
+
+fun three_seq_tr c [s1,s2,s3] =
+    Const(c,dummyT)$seq_tr s1$seq_tr s2$seq_tr s3;
+
+fun four_seq_tr c [s1,s2,s3,s4] =
+    Const(c,dummyT)$seq_tr s1$seq_tr s2$seq_tr s3$seq_tr s4;
+
+
+fun singlobj_tr'(Const("SeqO'",_)$fm) = fm |
+    singlobj_tr'(id) = Const("@SeqId",dummyT)$id;
+
+
+fun single_tr' c [s1, s2] =
+(Const (c, dummyT)$seq_tr' s1$seq_tr' s2 ); 
+
+
+fun two_seq_tr' c [s1, s2] =
+  Const (c, dummyT)$seq_tr' s1$seq_tr' s2; 
+
+fun three_seq_tr' c [s1, s2, s3] =
+  Const (c, dummyT)$seq_tr' s1$seq_tr' s2$seq_tr' s3; 
+
+fun four_seq_tr' c [s1, s2, s3, s4] =
+  Const (c, dummyT)$seq_tr' s1$seq_tr' s2$seq_tr' s3$seq_tr' s4; 
+
+
+