more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;

got rid of old error -- users who install SPASS manually are responsible for any version mismatches

tuned messages

natural component order

better error message

tuning

tuned

use only one data slot; rename print_quotmaps to print_quot_maps; tuned

merged

added rtrancl_while

renamed inner_dense_linorder to dense_linorder

renamed typeclass dense_linorder to unbounded_dense_linorder

tuned imports; tuned proofs;

another sample found by Stefan Berghofer;

added SHA1 library integrity test, which is invoked at compile time and Isabelle_Process run-time;

allow NUL characters in ML string passed to C library;

simplify code (now that ctr_sugar uses the same type variables as fp_sugar)

merged

prefer build_doc -s to avoid heaps left behind in $ISABELLE_HOME_USER (especially relevant to isatest);

prefer Binding.name_of over Binding.print -- the latter leads to funny quotes and markup within the constructed term;

always transfer thm where attributes are applied -- relevant for internal 'notes' (e.g. via bundle 'includes') in contrast to external 'notes' (cf. Proof_Context.retrieve_thms);

proper context;

tuned

moved derivation of ctor_dtor_unfold to sugar (streamlines fp_result interface)

export one more ML function, needed for primcorec

reverted 6c5e7143e1f6; took a better look at evaluation data this time

tuned unchecked ML;

removed junk;