tuned;

moved section "Document preparation" to front;

updated section "Markup via command tags";

renamed "formal comments" to "document comments"; tuned section "Markup commands"; updated/tuned section "Document Antiquotations";

renamed "formal comments" to "document comments";

tuned "Markup commands";

tuned intro of "Document preparation";

reworked "Defining Theories";

removed Assert.thy

dropped superfluos eval_conv

moved assert to Heap_Monad.thy

simproc for let

improved handling of !!/==> for eval and normalization

proper name morphisms for locales

consider prefixes for name bindings of simprocs (a first approximation)

diagnostic output for name bindings

Some modifications in code for proving arities to make it work for datatype definitions with additional sort constraints.

min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf

restruced naming code in anticipation of introduction of name morphisms

more verbose element printing

clarified comment

Added support for parametric datatypes.

Streamlined functions for accessing information about atoms.

Some more functions for accessing information about atoms.

Made doc compatible with the system.

clarified verbatim vs. typewriter

using explicit interpretaton prefix in Name.binding (still on the surface)

explicit interpretation prefix in Name.binding

tuned

exported codegen_preproc