discontinued unused end_line, end_column;

more scalable HTML.output_width;

refined comment (again);

merged

use proper syntactic types for 'syntax' commands

make print translation for Abs_cfun consistent with other binders: prevent eta-contraction, but don't force eta-expansion

use full path for library imports

types -> type_synonym

updated NEOS_SERVER, which is now provided via settings;

renamed Sum_Of_Squares to Sum_of_Squares;

Ord_List.merge convenience;

misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;

modernized structure Prop_Logic; avoid ML structure aliases;

added Context_Position.is_visible_proof, which treats a global theory as invisible (unlike the default);

tuned;

tuned;

tuned headers;

merged

adding example theory for list comprehension to set comprehension simproc

adopting proofs due to new list comprehension to set comprehension simproc

adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs

tuned text

merged

removing obselete Id comments from HOL/ex theories

added hints about licensing restrictions and how to enable Z3

tuned

eliminated hard tabs;

allow spaces in $SPASS_HOME value;

tuned;

eliminated alias;