domain package:
* theorems are stored in the theory
* creates hierachical name space
* minor changes to some names and values (for consistency),
e.g. cases -> casedist, dists_eq -> dist_eqs,
[take_lemma] -> take_lemmas
* separator between mutual domain definitions changed from "," to "and"
* minor debugging of Domain_Library.mk_var_names
(* Title: HOLCF/stream2.thy
ID: $Id$
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
Additional constants for stream
*)
Stream2 = Stream +
consts
smap :: "('a -> 'b) -> 'a stream -> 'b stream"
rules
smap_def
"smap = fix[LAM h f s. stream_when[LAM x l.scons[f[x]][h[f][l]]][s]]"
end
(*
smap[f][UU] = UU
x~=UU --> smap[f][scons[x][xs]] = scons[f[x]][smap[f][xs]]
*)