src/HOLCF/ex/Dagstuhl.thy
author wenzelm
Mon, 23 Oct 2000 22:17:55 +0200
changeset 10313 51e830bb7abe
parent 2570 24d7e8fb8261
child 10835 f4745d77e620
permissions -rw-r--r--
intro_classes by default; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2570
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
     1
(* $Id$ *)
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
     2
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
     3
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
     4
Dagstuhl  =  Stream +
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
     5
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
     6
consts
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
     7
        y  :: "'a"
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
     8
       YS  :: "'a stream"
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
     9
       YYS :: "'a stream"
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    10
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    11
defs
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    12
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    13
YS_def    "YS  == fix`(LAM x. y && x)"
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    14
YYS_def   "YYS == fix`(LAM z. y && y && z)"
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    15
  
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    16
end
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    17