fixed title line; added spacing
authorpaulson
Fri Jun 11 10:35:55 1999 +0200 (1999-06-11)
changeset 6819433a980103b4
parent 6818 852f9ed01a53
child 6820 41d9b7bbf968
fixed title line; added spacing
src/Sequents/Sequents.thy
     1.1 --- a/src/Sequents/Sequents.thy	Fri Jun 11 10:34:20 1999 +0200
     1.2 +++ b/src/Sequents/Sequents.thy	Fri Jun 11 10:35:55 1999 +0200
     1.3 @@ -1,4 +1,4 @@
     1.4 -(*  Title: 	LK/lk.thy
     1.5 +(*  Title: 	Sequents/Sequents.thy
     1.6      ID:         $Id$
     1.7      Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.8      Copyright   1993  University of Cambridge
     1.9 @@ -61,20 +61,20 @@
    1.10  
    1.11  fun abs_seq' t = Abs("s", Type("seq'",[]), t);
    1.12  
    1.13 -fun seqobj_tr(Const("SeqO",_)$f) = Const("SeqO'",dummyT)$f |
    1.14 -    seqobj_tr(_$i) = i;
    1.15 +fun seqobj_tr(Const("SeqO",_) $ f) = Const("SeqO'",dummyT) $ f |
    1.16 +    seqobj_tr(_ $ i) = i;
    1.17      
    1.18  fun seqcont_tr(Const("SeqContEmp",_)) = Bound 0 |
    1.19 -    seqcont_tr(Const("SeqContApp",_)$so$sc) = 
    1.20 -      (seqobj_tr so)$(seqcont_tr sc);
    1.21 +    seqcont_tr(Const("SeqContApp",_) $ so $ sc) = 
    1.22 +      (seqobj_tr so) $ (seqcont_tr sc);
    1.23  
    1.24  fun seq_tr(Const("SeqEmp",_)) = abs_seq'(Bound 0) |
    1.25 -    seq_tr(Const("SeqApp",_)$so$sc) = 
    1.26 -      abs_seq'(seqobj_tr(so)$seqcont_tr(sc));
    1.27 +    seq_tr(Const("SeqApp",_) $ so $ sc) = 
    1.28 +      abs_seq'(seqobj_tr(so) $ seqcont_tr(sc));
    1.29  
    1.30  
    1.31 -fun singlobj_tr(Const("SeqO",_)$f) =
    1.32 -    abs_seq' ((Const("SeqO'",dummyT)$f)$Bound 0);
    1.33 +fun singlobj_tr(Const("SeqO",_) $ f) =
    1.34 +    abs_seq' ((Const("SeqO'",dummyT) $ f) $ Bound 0);
    1.35      
    1.36  
    1.37      
    1.38 @@ -82,66 +82,66 @@
    1.39  
    1.40  fun seqcont_tr' (Bound 0) = 
    1.41        Const("SeqContEmp",dummyT) |
    1.42 -    seqcont_tr' (Const("SeqO'",_)$f$s) =
    1.43 -      Const("SeqContApp",dummyT)$
    1.44 -      (Const("SeqO",dummyT)$f)$
    1.45 +    seqcont_tr' (Const("SeqO'",_) $ f $ s) =
    1.46 +      Const("SeqContApp",dummyT) $ 
    1.47 +      (Const("SeqO",dummyT) $ f) $ 
    1.48        (seqcont_tr' s) |
    1.49 -(*    seqcont_tr' ((a as Abs(_,_,_))$s)= 
    1.50 +(*    seqcont_tr' ((a as Abs(_,_,_)) $ s)= 
    1.51        seqcont_tr'(betapply(a,s)) | *)
    1.52 -    seqcont_tr' (i$s) = 
    1.53 -      Const("SeqContApp",dummyT)$
    1.54 -      (Const("SeqId",dummyT)$i)$
    1.55 +    seqcont_tr' (i $ s) = 
    1.56 +      Const("SeqContApp",dummyT) $ 
    1.57 +      (Const("SeqId",dummyT) $ i) $ 
    1.58        (seqcont_tr' s);
    1.59  
    1.60  fun seq_tr' s =
    1.61      let fun seq_itr' (Bound 0) = 
    1.62                Const("SeqEmp",dummyT) |
    1.63 -            seq_itr' (Const("SeqO'",_)$f$s) =
    1.64 -              Const("SeqApp",dummyT)$
    1.65 -              (Const("SeqO",dummyT)$f)$(seqcont_tr' s) |
    1.66 -(*            seq_itr' ((a as Abs(_,_,_))$s) =
    1.67 +            seq_itr' (Const("SeqO'",_) $ f $ s) =
    1.68 +              Const("SeqApp",dummyT) $ 
    1.69 +              (Const("SeqO",dummyT) $ f) $ (seqcont_tr' s) |
    1.70 +(*            seq_itr' ((a as Abs(_,_,_)) $ s) =
    1.71                seq_itr'(betapply(a,s)) |    *)
    1.72 -            seq_itr' (i$s) =
    1.73 -              Const("SeqApp",dummyT)$
    1.74 -              (Const("SeqId",dummyT)$i)$
    1.75 +            seq_itr' (i $ s) =
    1.76 +              Const("SeqApp",dummyT) $ 
    1.77 +              (Const("SeqId",dummyT) $ i) $ 
    1.78                (seqcont_tr' s)
    1.79      in case s of 
    1.80           Abs(_,_,t) => seq_itr' t |
    1.81 -         _ => s$(Bound 0)
    1.82 +         _ => s $ (Bound 0)
    1.83      end;
    1.84  
    1.85  
    1.86  
    1.87  
    1.88  fun single_tr c [s1,s2] =
    1.89 -    Const(c,dummyT)$seq_tr s1$singlobj_tr s2;
    1.90 +    Const(c,dummyT) $ seq_tr s1 $ singlobj_tr s2;
    1.91  
    1.92  fun two_seq_tr c [s1,s2] =
    1.93 -    Const(c,dummyT)$seq_tr s1$seq_tr s2;
    1.94 +    Const(c,dummyT) $ seq_tr s1 $ seq_tr s2;
    1.95  
    1.96  fun three_seq_tr c [s1,s2,s3] =
    1.97 -    Const(c,dummyT)$seq_tr s1$seq_tr s2$seq_tr s3;
    1.98 +    Const(c,dummyT) $ seq_tr s1 $ seq_tr s2 $ seq_tr s3;
    1.99  
   1.100  fun four_seq_tr c [s1,s2,s3,s4] =
   1.101 -    Const(c,dummyT)$seq_tr s1$seq_tr s2$seq_tr s3$seq_tr s4;
   1.102 +    Const(c,dummyT) $ seq_tr s1 $ seq_tr s2 $ seq_tr s3 $ seq_tr s4;
   1.103  
   1.104  
   1.105 -fun singlobj_tr'(Const("SeqO'",_)$fm) = fm |
   1.106 -    singlobj_tr'(id) = Const("@SeqId",dummyT)$id;
   1.107 +fun singlobj_tr'(Const("SeqO'",_) $ fm) = fm |
   1.108 +    singlobj_tr'(id) = Const("@SeqId",dummyT) $ id;
   1.109  
   1.110  
   1.111  fun single_tr' c [s1, s2] =
   1.112 -(Const (c, dummyT)$seq_tr' s1$seq_tr' s2 ); 
   1.113 +(Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2 ); 
   1.114  
   1.115  
   1.116  fun two_seq_tr' c [s1, s2] =
   1.117 -  Const (c, dummyT)$seq_tr' s1$seq_tr' s2; 
   1.118 +  Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2; 
   1.119  
   1.120  fun three_seq_tr' c [s1, s2, s3] =
   1.121 -  Const (c, dummyT)$seq_tr' s1$seq_tr' s2$seq_tr' s3; 
   1.122 +  Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2 $ seq_tr' s3; 
   1.123  
   1.124  fun four_seq_tr' c [s1, s2, s3, s4] =
   1.125 -  Const (c, dummyT)$seq_tr' s1$seq_tr' s2$seq_tr' s3$seq_tr' s4; 
   1.126 +  Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2 $ seq_tr' s3 $ seq_tr' s4; 
   1.127  
   1.128  
   1.129