rudimentary code setup for set operations

<applet>: more XHTML 1.0 Transitional conformance;

Isar.command: OuterSyntax.prepare_command_failsafe defers syntax errors until execution time;

<pre>: removed xml:space, is already default; result(s): avoid improper nesting of <pre> within <p>;

produce XHTML 1.0 Transitional; tuned charset name; renamed Markup.class to Markup.tclass, to avoid potential conflicts with spacial meaning in markup languages (e.g. HTML);

renamed Markup.class to Markup.tclass, to avoid potential conflicts with spacial meaning in markup languages (e.g. HTML);

Isar.command: do not set position of enclosing transaction, to avoid of clash with the one being prepared here!

changed code setup

re-arranged class dense_linear_order

rudimentary code setup for set operations

moved class wellorder to theory Orderings

added parse_token (from proof_context.ML);

read_tyname/const/const_proper: report position; moved parse_token to syntax.ML; tuned;

pass position to get_fact; tuned;

pass token source to typ/term etc.;

added name property operation; added local_fact; renamed proposition to prop (again);

renamed ML_Lex.val_of to content_of;

unified Args.T with OuterLex.token, renamed some operations; moved thm_sel to attrib.ML;

unified Args.T with OuterLex.token; RESET_VALUE of primitive parsers; export keyword_with; renamed keyword_sid to keyword_ident_or_symbolic; added int (from args.ML); added enum(1)', and_list(1)' (formerly in args.ML); removed obsolete arguments/generic_args1 (cf. parse/parse1 in args.ML);

unified Args.T with OuterLex.token; renamed val_of to content_of; added InternalValue kind; added datatype value/slot with static binding (from args.ML); renamed is_sid to ident_or_symbolic;

unified Args.T with OuterLex.token, renamed some operations; removed obsolete parse_args (cf. parse);

unified Args.T with OuterLex.token, renamed some operations; unified version of thm_sel (formerly in args.ML and spec_parse.ML);

unified Args.T with OuterLex.token; moved datatype value/slot and basic operations to outer_lex.ML; removed unused terminator; removed obsolete !!!, position, nat, int, list(1), enum(1) and_list(1) (cf. outer_parse.ML); removed obsolete thm_sel (cf. attrib.ML); one unified version of parse/parse1 (formerly arguments/generic_args1 in outer_parse.ML);

load args.ML later (after outer_parse.ML);

unified Args.T with OuterLex.token, renamed some operations;

read_asts: report literal tokens;

tuned error message;

pos_of_token: Position.T; removed unused display_token; tuned;

dest: sort strings; report: Output.status;

added literal;