| author | oheimb | 
| Thu, 30 Aug 2001 15:47:30 +0200 | |
| changeset 11507 | 4b32a46ffd29 | 
| parent 11355 | 778c369559d9 | 
| child 14981 | e73f8140af78 | 
| permissions | -rw-r--r-- | 
| 11350 
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
 oheimb parents: diff
changeset | 1 | (* Title: HOLCF/FOCUS/FOCUS.thy | 
| 11355 | 2 | ID: $Id$ | 
| 11350 
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
 oheimb parents: diff
changeset | 3 | Author: David von Oheimb, TU Muenchen | 
| 
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
 oheimb parents: diff
changeset | 4 | License: GPL (GNU GENERAL PUBLIC LICENSE) | 
| 
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
 oheimb parents: diff
changeset | 5 | |
| 
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
 oheimb parents: diff
changeset | 6 | top level of FOCUS | 
| 
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
 oheimb parents: diff
changeset | 7 | *) | 
| 
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
 oheimb parents: diff
changeset | 8 | |
| 
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
 oheimb parents: diff
changeset | 9 | FOCUS = Fstream |