ordered lists instead of tables for resolving hyps; speedup

nominal_primrec now prints initial proof state.

Abbreviations can now be specified simultaneously with introduction rules.

Adapted to new inductive definition package.

added ProofGeneral settings;

tuned comments;

tuned;

defs: increased entropy of mixfix handling;

fixed term_of_list;

Concrete syntax for hex chars and strings.

renamed str_of_XXX to print_XXX;

HOLogic cleanup;

ML_Syntax.print_XXX;

misc cleanup -- removed non-HOL operations; nibble/char/list/string: observe conventions for abstract syntax operations;

moved char/string syntax to Tools/string_syntax.ML; HOLogic cleanup;

added Tools/string_syntax.ML; tuned;

removed junk;

interpretation: use C_class name prefix;

abs/binder_tr': support printing of idtdummy;

respects2: tuned spacing;

support printing of idtdummy;

added is_class (approximation); added abbrev; tuned;

LocalTheory.notation/abbrev;

extract_case: Name.clean;

added target_notation/abbrev; tuned;

added notation/abbrev (from term_syntax.ML);

tuned absdummy;

added no_frees; add_abbrev: tuned handling of frees, temp workaround;

removed (cf. proof_context.ML and local_theory.ML);

removed Isar/term_syntax.ML;

avoid internal name O_;

hide const linorder.less_eq_less.max linorder.less_eq_less.min;

hardwired option -q;

added print_abbrevs; tuned;

renaming

Modified lattice locale

updated;

added internal_mode;

simplified abbrev: single argument;

TermSyntax.abbrev; ProofContext.set_expand_abbrevs;

added read/pretty_term_abbrev, print_abbrevs; tuned Consts signature; renamed expand_abbrevs to set_expand_abbrevs;

init_context: reset naming;

added 'print_abbrevs';

added print_abbrevs; exit: less verbosity;

added term_abbrev;

renamed reserved to reserved_names; added reserved: Name.context;

tuned Consts signature;

abbrevs: print original rhs;

abbreviate: always authentic, force expansion of internal abbreviations; tuned signature; tuned;

ML_Syntax.reserved(_names);

TermSyntax.abbrev;

added antiquotation abbrev;

added print_abbrevs;

tuned use_text; eval command line: skip over -q option;

added 'help' command (same of 'print_commands');

more careful evaluation of ML text, prevents spurious output;