Regression tests for new locale implementation.

add_locale functional.

Added a line that was missing from the definition

added binary logarithm

Strange. The proof worked in the 2008 release. In order to make it work now, the last line of the proof must be moved up two places. In other words, the first proof step is now returning its subgoals in a different order from before.

Name.binding

added optimizer

reactivated some dead theories (based on hints by Mark Hillebrand);

Locale.local_note_qualified

fact table now using name bindings

dropped legacy naming code

tuned name bindings

using name bindings

name spaces and name bindings

Deleted debug message (PolyML).

removed traces of former 'includes' element;

updated generated files;

Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;

*** empty log message ***

fixed

Added new fold operator and renamed the old oe to fold_image.

Type inference for elements through syntax module.

Use 'if' in connection with 'is_some' and 'the'.

Basic types not qualified.

Enable switching to new locales during session.

explicit inhabitance proof

fulfill_proof/thm_proof: commuted lazyness; join_futures: Exn.release_all is back again (still required for implicit join of Toplevel.excursion);

fulfill_proof/thm_proof: commuted lazyness;

removed lemmas called lemma1 and lemma2

force_proofs after cumulative use_thys; PureThy.force_proofs;