Adopted output of values command

improved handling of overloaded constants; examples with numerals

made SML/NJ happy; tuned

adding tracing function for evaluated code; annotated compilation in the predicate compiler

added documentation for local SMT solver setup and available SMT options, added verbose output for SMT solver invocation, test if local SMT solver exists before invoking it, always trace (possible) counterexamples, documented existence of SMT server

renamed method induct_scheme to induction_schema

NEWS

removed session SizeChange: outdated, only half-functional, alternatives exist (cf. size_change method)

renamed method sizechange to size_change

added boehmes and hoelzl to isatest mailings

merged

tuned

Merged.

Merged.

Use PrintMode.setmp to make thread-safe; avoid code clones.

Make output indenpendent of current print mode.

Relax on type agreement with original context when applying term syntax.

tuned;

proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context; tuned signature; tuned;

adapted LocalTheory.declaration;

allow "pervasive" local theory declarations, which are applied the background theory;

declare Spec_Rules for most basic definitional packages;

misc tuning and clarification;

scalable version of Named_Thms, using Item_Net;

merged

merged

more accurate cleanup;

merged

more accurate dependencies;

merged