src/HOLCF/ex/Dagstuhl.thy
author regensbu
Tue, 07 Feb 1995 17:35:49 +0100
changeset 896 56b9c2626e81
parent 299 febeb36a4ba4
child 1168 74be52691d62
permissions -rw-r--r--
ID for the file
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
896
56b9c2626e81 ID for the file
regensbu
parents: 299
diff changeset
     1
(* $Id$ *)
56b9c2626e81 ID for the file
regensbu
parents: 299
diff changeset
     2
299
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
     3
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
     4
Dagstuhl  =  Stream2 +
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
     5
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
     6
consts
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
     7
       YS  :: "'a stream"
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
     8
       YYS :: "'a stream"
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
     9
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    10
rules
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    11
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    12
YS_def    "YS  = fix[LAM x. scons[y][x]]"
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    13
YYS_def   "YYS = fix[LAM z. scons[y][scons[y][z]]]"
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    14
  
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    15
end
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    16