No interpretation of locale with dangling type frees.

Do not rely on locale assumption in interpretation.

The metis method now fails in the usual manner, rather than raising an exception, if it determines that it cannot prove the theorem.

Fixed typo in locale declaration.

added babel

explicit size of characters

dropped superfluous code lemmas

evaluation using code generator

generic value command

converted symbols.tex;

tuned;

converted misc.tex;

tuned;

generated files;

converted present.tex;

basic setup for generated document sources (cf. IsarRef/isar-ref.tex);

load underscore package after iman etc.;

tuned comment;

added formal markup for setting, executable, tool;

basic setup for generated document sources (cf. IsarRef/isar-ref.tex);

converted basics.tex to theory file;

added isatt markup;

New outline for codegen tutorial -- draft

added extern_fact (local or global); more procise printing of fact names;