src/HOL/New_DSequence.thy
changeset 39183 512c10416590
parent 36902 c6bae4456741
child 40049 75d9f57123d6
     1.1 --- a/src/HOL/New_DSequence.thy	Mon Sep 06 15:01:37 2010 +0200
     1.2 +++ b/src/HOL/New_DSequence.thy	Tue Sep 07 11:51:53 2010 +0200
     1.3 @@ -83,7 +83,7 @@
     1.4  
     1.5  definition pos_not_seq :: "unit neg_dseq => unit pos_dseq"
     1.6  where
     1.7 -  "pos_not_seq xq = (%i. Lazy_Sequence.hb_not_seq (xq i))"
     1.8 +  "pos_not_seq xq = (%i. Lazy_Sequence.hb_not_seq (xq (3 * i)))"
     1.9  
    1.10  definition neg_not_seq :: "unit pos_dseq => unit neg_dseq"
    1.11  where