src/HOLCF/FOCUS/FOCUS.thy
author huffman
Thu, 31 Mar 2005 02:44:46 +0200
changeset 15638 1fb24e545f88
parent 14981 e73f8140af78
child 17293 ecf182ccc3ca
permissions -rw-r--r--
fixed bug in prj' function
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
11350
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
     1
(*  Title: 	HOLCF/FOCUS/FOCUS.thy
11355
wenzelm
parents: 11350
diff changeset
     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
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
     5
top level of FOCUS
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
     6
*)
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
FOCUS = Fstream