equal
deleted
inserted
replaced
1 (* Title: Pure/General/seq.ML |
1 (* Title: Pure/General/seq.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Author: Markus Wenzel, TU Munich |
4 Author: Markus Wenzel, TU Munich |
5 License: GPL (GNU GENERAL PUBLIC LICENSE) |
|
6 |
5 |
7 Unbounded sequences implemented by closures. RECOMPUTES if sequence |
6 Unbounded sequences implemented by closures. RECOMPUTES if sequence |
8 is re-inspected. Memoing, using polymorphic refs, was found to be |
7 is re-inspected. Memoing, using polymorphic refs, was found to be |
9 slower! (More GCs) |
8 slower! (More GCs) |
10 *) |
9 *) |