eliminated obsolete "internal" kind -- collapsed to unspecific "";

unused_thms: ignore kind -- already observes "concealed" flag;

all_valid_thms: more sophisticated check against global + local name space;

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