--- 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)"