# HG changeset patch
# User mueller
# Date 880472060 -3600
# Node ID d30fbe1296831bd02f8820e1a60cb5c66cea4791
# Parent  6c6073b13600592213b7eb2bf79996f9198b18da
resolved merge conflict;

diff -r 6c6073b13600 -r d30fbe129683 src/HOLCF/IOA/meta_theory/Seq.thy
--- a/src/HOLCF/IOA/meta_theory/Seq.thy	Mon Nov 24 16:43:43 1997 +0100
+++ b/src/HOLCF/IOA/meta_theory/Seq.thy	Tue Nov 25 16:34:20 1997 +0100
@@ -29,6 +29,7 @@
    Infinite      ::"'a seq => bool"
 
    nproj        :: "nat => 'a seq => 'a"
+   sproj        :: "nat => 'a seq => 'a seq"
 
 syntax
    "@@"		:: "'a seq => 'a seq => 'a seq"	(infixr 65)
@@ -103,10 +104,16 @@
              | x##xs => (case t2 of 
                           nil => UU 
                         | y##ys => <x,y>##(h`xs`ys))))"
+ 
+
+nproj_def 
+ "nproj == (%n tr.HD`(iterate n TL tr))"   
 
 
-proj_def 
- "nproj == (%n tr. HD`(iterate n TL tr))"   
+sproj_def 
+ "sproj == (%n tr.iterate n TL tr)"   
+
+
 
 Partial_def
   "Partial x  == (seq_finite x) & ~(Finite x)"