added interface of user proposals for names of generated constants

first steps towards a new mode datastructure; new syntax for mode annotations and new output of modes

adding more tests for the values command; adding some forbidden constants to inductify * * * added further testcase for values command

Enables tests for locale functionality that is now available.

merged

uniform use of simultabeous use_thys;

merged

explicit invocation of code generation

adding code equations for constructors

tuned

changed URL of SMT server, added Z3 rewrite lemma

Added two new lemmas

tuned imports

tuned

local mutex for theory content/identity operations;

admit dummy implementation;

Toplevel.thread provides Isar-style exception output;

generalized Runtime.toplevel_error wrt. output function;

exported SimpleThread.attributes;

plain add_preference, no setmp_CRITICAL required;

adapted Theory_Data;

recovered update from 7264824baf66, which got lost in 7264824baf66;

merged

merged

tuned header

substantial simplification restores code generation

lemmas about apfst and apsnd

tuned imports