removed rather toyish tree

updated keywords

merged

user interface for abstract datatypes is an attribute, not a command

implementation of mappings by rbts

lemma is_empty_empty

constructor Mapping replaces AList

stay within Local_Defs layer;

expose foundational typedef axiom name;

Thm.add_axiom/add_def: return internal name of foundational axiom;

modernized datatype constructors;

of_sort_derivation: weaken bypasses derivation for identical sort -- accomodate proof terms by krauss/schropp, for example;

tuned;

of_sort_derivation: pass-through full type information -- following the version by krauss/schropp;

include JEDIT_APPLE_PROPERTIES by default;

isatest: more uniform setup for Unix vs. Cygwin;

added missing case: meta universal quantifier

added imperative SAT checker; improved headers of example files; adopted IsaMakefile

Merged.

Merged resolving conflicts NEWS and locale.ML.

Proper inheritance of mixins for activated facts and locale dependencies.

Removed obsolete function.

Graceful treatment of non-locale subgoals by methods unfold_locales and intro_locales.

Tuned interpretation proofs.

A rough implementation of full mixin inheritance; additional unit tests.

Clarified invariant; tuned.

More mixin tests.

Use serial to be more debug friendly.

buffered output (faster than direct output)

simplified Cache_IO interface (input is just a string and not already stored in a file)