src/HOLCF/ex/Dagstuhl.thy
author berghofe
Mon, 19 Nov 2001 17:36:05 +0100
changeset 12233 3348aa8061d1
parent 10835 f4745d77e620
child 17291 94f6113fe9ed
permissions -rw-r--r--
- Fixed bug in shrink - Restored old behaviour of thm_proof - Eliminated reference from theory data
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
10835
nipkow
parents: 2570
diff changeset
    13
YS_def    "YS  == fix$(LAM x. y && x)"
nipkow
parents: 2570
diff changeset
    14
YYS_def   "YYS == fix$(LAM z. y && y && z)"
2570
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