Although full access to the FDL content will be effected by APIs, for the purpose of showing the structure of this material, it is projected onto the web showing references between the individual objects. Each inference step of a proof is presented as a single page with links to its children and ancestors. For convenience, each theorem statement is also directly linked to all the inference steps of its proof.
Each theory page is linked in the upper righthand corner to the ascii *.pvs source for the theory (the whole collection of theories in the Prelude is, however, from a single file).
Improvements to come: more theories will be presented (now only the theory collections from the standard Prelude through Graphs are presented); cross referencing will be introduced (now only direct mention of one entity by another is presented).
