Antiq: inner vs. outer position; scan_antiq: use T.scan_quoted;

of_properties: observe Markup.position_properties';

added position_properties'; renamed prop to proposition; added attribute, method;

token: maintain of source, which retains original position information; removed count/counted, advance position via scanned source;

moved OuterLex.count here;

improved recover: also resync on symbol/comment/verbatim delimiters;

advance: operate on symbol list (less overhead);

added token;

fix HOL/ex/LexOrds.thy; add to regression

added report;

removed axiom; added fact, dynamic_fact, prop;

get_fact: report position;

Facts.lookup: return static/dynamic status;

position scanner: encode token range;

added encode_range; tuned;

added end_line, end_column properties;

meta_subst: xsymbols make it work with clean Pure;

abstract type Scan.stopper, position taken from last input token;

abstract type Scan.stopper;

abstract type stopper, may depend on final input;

removed obsolete apply_theorems(_i);

tuned signature; eliminated obsolete pervasives;

removed obsolete note_thms_cmd;

simplified defer_recdef(_i): plain facts via Attrib.eval_thms;

tuned description;

replaced mercurial.cgi by hgwebdir.cgi, resulting in http://isabelle.in.tum.de/repos/isabelle/

Quoted terms in consts_code declarations are now preprocessed as well.

Exported eval_wrapper.

- corrected bogus comment for function inst_conj_all - tuned function obtain_fresh_name

removed dead code