pred_subset_eq and SUP_UN_eq2 are now standard pred_set_conv rules

pred_subset/equals_eq are now standard pred_set_conv rules

Declared pred_equals/subset_eq, sup_Un_eq and SUP_UN_eq(2) as pred_set_conv rules

merged

add simp rules for set_bit and msb applied to 0 and 1

add simp rule test_bit_1

proper hiding of facts and constants in AList_Impl and AList theory

NEWS

adding quickcheck examples with multisets

improving code generation for multisets; adding exhaustive quickcheck generators for multisets

adding theory association lists with invariant

command status color via regular markup;

proper cumulation of bulk arguments;

tuned;

merge

revert unintended "sledgehammer" call

prefer antiquotations;

misc tuning and reformatting;

updated generated file;

Added termination to IMP Abs_Int

added lemmas

massaging of code setup for sets

dropped theory More_Set

use Inf/Sup_bool_def/apply as code equations

tuned

accumulate status as regular markup for command range; tuned signature;

corrected slip

tuned

restore convenient code_abbrev declarations (particulary important if List.set is not the formal constructor for sets)

moved lemmas about List.set and set operations to List theory

moved lemmas about List.set and set operations to List theory

incorporated various theorems from theory More_Set into corpus