src/HOLCF/ex/Dagstuhl.thy
author lcp
Tue, 16 Aug 1994 19:09:43 +0200
changeset 536 5fbfa997f1b0
parent 299 febeb36a4ba4
child 896 56b9c2626e81
permissions -rw-r--r--
ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where they can be proved trivially using eq_cs ZF/domrange/XXX_empty: renamed XXX_0
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
299
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
     1
(*
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
     2
    ID:         $ $
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
     3
*)
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
     4
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
     5
Dagstuhl  =  Stream2 +
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
     6
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
     7
consts
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
     8
       YS  :: "'a stream"
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
     9
       YYS :: "'a stream"
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    10
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    11
rules
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    12
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    13
YS_def    "YS  = fix[LAM x. scons[y][x]]"
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    14
YYS_def   "YYS = fix[LAM z. scons[y][scons[y][z]]]"
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    15
  
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    16
end
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    17