Proof General / Emacs interface wrapper;

Proof General: option -I is obsolete;

added PROOFGENERAL_HOME;

separate emacs tool for Proof General / Emacs;

added quickcheck stub

removed babel again

celver code lemma avoid type ambiguity problem with Haskell

a sophisticated char/nibble conversion combinator

moved term_of syntax to separate theory

SimpleThread.fork;

Simplified thread fork interface.

added Concurrent/simple_thread.ML;

updated generated file;

misc tuning and modernization;

check setting and tool; added file;

Clearer separation of interpretation frontend and backend.

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;

print raw (internal) result names;

more procise printing of fact names;

pretty_fact: extern fact name wrt. the given context, assuming that is the proper one for presentation;

cancel, shutdown: notify_all;

finish: Future.shutdown last;

eliminated requests, use global state variables uniformly; more robust shutdown;

finish: Future.shutdown;

added is_empty;