| author | kleing | 
| Mon, 14 Jul 2003 14:44:06 +0200 | |
| changeset 14110 | c45c94fa16f4 | 
| 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 |