uniform bookkeeping also in the case of deletion

more abstract declaration of code attributes

dropped unused material

proper context for norm_hhf and derived operations; clarified tool context in some boundary cases;

made SML/NJ happy;

added system option "jedit_print_mode";

avoid hardwired /bin/bash (like canonical Isabelle shell scripts);

tuned whitespace;

simplified

more compact representation of different situations for interpretation

more succint formulation of special case

tuned whitespace

move instantiation here from AFP/Native_Word

dropped junk

postpone dis"useful" lemmas

cleanup

prefix disambiguation

tuned proofs and declarations

prefer target-style syntaxx for sublocale

prefer ephemeral interpretation over interpretation in proof contexts; prefer context begin ... end blocks for often-occuring assumptions; slightly more complete interpretations into abstract algebraic structures for gcd/lcm

self-contained formulation of subclass command, avoiding hard-wired Named_Target.init

ephemeral interpretation also formally works on theory level

abolished slightly odd global lattice interpretation for min/max

prefer more canonical names for lemmas on min/max

explicit distributivity facts on min/max

postponed min/max lemmas until abstract lattice is available

tuned structure of min/max lemmas

prefer abstract simp rule

more lemmas on abstract lattices

tuning and augmentation of min/max lemmas; more lemmas and simp rules for abstract lattices with order; tuned proofs