basic scanners: produce symbol list instead of imploded string; tuned signature;

* Outer syntax: string tokens no longer admit escaped white space;

location_of_position: Position.column_of (which counts Isabelle symbols, not characters);

added count/counted: improved position handling for token syntax; removed obsolete incr_line/keep_line/scan_blank; string tokens no longer admit escaped white space, which was an accidental (undocumented) feature;

added column field; replaced inc by general advance operation; str_of: no output for file without line information;

T.count/counted: improved position handling for token syntax;

added column property;

removed redundant repeatd scanner combinator;

added ::: / @@@ scanner combinators;

Tuned uniqueness proof for recursion combinator.

Cleaned up simproc code.

tuned the proof of the substitution lemma

rename_client_map_tac: avoid ill-defined thm reference;

use_thy: do not set implicit ML context anymore;

added ambiguity_limit (restricts parse trees / terms printed in messages); tuned;

renamed thms_containing_limit to FindTheorems.limit;

eliminated some legacy ML files;

added bind_thms;

tuned;

removed legacy ML file;

syntax error: unified output of priorities;

syntax error: reduced spam -- print expected nonterminals instead of terminals; tuned pretty_gram;

avoid redundant escaping of Isabelle symbols;

grouped versions of axioms/define/notes;

misc tuning and internal rearrangement; tuned attribute syntax -- no need for eta-expansion;

added theorem group property;

added theorem group operations; note_thmss: add kind to *all* intermediate thms; get_kind: default to empty name;

added surround;