- Proofs are now hidden by default when generating documents
- New syntax for referring to theorems in lists
- Improvements to theory loader (relative and absolute paths)
(* $Id$ *)
Dagstuhl = Stream +
consts
y :: "'a"
YS :: "'a stream"
YYS :: "'a stream"
defs
YS_def "YS == fix$(LAM x. y && x)"
YYS_def "YYS == fix$(LAM z. y && y && z)"
end