Remove map_compose, replaced by map_map

New list theorems; added map_map to simpset, this is the prefered direction; allow sorting by a key

Renamed upd_snd_conv to apsnd_conv to be consistent with apfst_conv; Added apsnd_apfst_commute

merged

accomplish mutual recursion between fun and inst

moved lemma map_of_zip_map to Map.thy

merged

explicit code lemmas produce nices code

repaired broken code_const for term_of [String.literal]

fixed soundness bug in Nitpick related to sets

removed unnecessary oracle in the predicate compiler

improving code quality thanks to Florian's code review

renaming code_pred_intros to code_pred_intro * * * adopted alternative definitions for the predicate compiler to new attribute name

announcing the predicate compiler in NEWS and CONTRIBUTORS

new names for predicate functions in the predicate compiler * * * adopting examples of the predicate compiler

removed deprecated mode annotation parser; renamed accepted mode annotation parser to nicer naming

added another example to the predicate compiler * * * tuning examples

changed modes to expected_modes; added UNION to code_pred_inlining; fixed some examples; tuned

removed dummy setup for predicate compiler commands as the compiler is now part of HOL-Main

adopted predicate compiler examples to new syntax for modes

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