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