Removal of the "keep_types" flag: we always keep types!

make SML/NJ happy;

made SML/NJ happy;

consistent naming for FreeUltrafilterNat lemmas; cleaned up

cleaned up; generalized some proofs

fix assumptions on NSDERIV_quotient

changed (ns)deriv to take functions of type 'a::real_normed_field => 'a

generalize some theorems

add type annotation

read_xnum: return leading_zeros, radix;

authentic syntax for Pls/Min/Bit; separated translation functions from HOLogic functionality;

authentic syntax for Pls/Min/Bit;

binary numerals: restricted to actual abstract syntax; tuned;

Hyperreal/FrechetDeriv.thy

theory of Frechet derivatives

specials: include single quote;

xstr: disallow backslashes;

advanced translation functions: Proof.context; abs/binder_tr: disallow internal names for bounds;

advanced translation functions: Proof.context;

added improved versions of use_text/file (still inactive);

added use_file;

load secure.ML after symbol.ML, when default output is active;

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;

date: forcing LC_ALL=C prevents funny file names;

root function: restore default interrupt handler; output file: avoid .exe (e.g. for Cygwin);

patched up the proofs agsin

removed use of put_name_hint, as the ATP linkup no longer needs this

reorganized structure Tactic vs. MetaSimplifier;

begin/end blocks; tuned notation;

abbrevs: more careful interpretation, avoid dynamic references to local names;

definition/abbreviation: single argument;

simplified add_abbrev -- single argument;

removed obsolete references to ProofGeneral/isa;

added input_mode;

tuned print_locale output; add_decls: Thm.internalK;

moved notation/abbrevs to TermSyntax;

expand_term: based on Envir.expand_term; tuned;

thms etc.: proper treatment of internal_fact with selection;

tuned pretty_src output;

simplified add_abbrevs: no mixfix;

added expand_term;

tuned;

Common term syntax declarations.

added Isar/term_syntax.ML;

TermSyntax.notation/abbrevs;

Removal of theorem tagging, which the ATP linkup no longer requires. Suffixes no longer blacklisted.

Removal of theorem tagging, which the ATP linkup no longer requires,

Poly/ML 5.0 setup for Isabelle2005.

reorganized structure Goal vs. Tactic;

export: added explicit term operation;

abbrevs: actually observe target_morphism;

added expand; export: added explicit term operation;

moved hidden_polymorphism to term.ML;

added hidden_polymorphism (from variable.ML);

add_abbrevs: moved common parts to consts.ML;

abbreviate: improved error handling, return result;

export: added explicit term operation; tuned export_morphism -- lean closure;

LocalDefs.expand;

Improved tracing

no timing;

simplified ML bindings;

simplified ML bindings -- moved to HOL.thy; removed confusing simpset_basic/simplify;

added basic ML bindings;

added aliases for nat_recs/cases;

removed legacy ML bindings; simplified ML setup; tuned declarations;