2006-12-09 wenzelm 2006-12-09 updated;
2006-12-09 wenzelm 2006-12-09 added internal_mode;
2006-12-09 wenzelm 2006-12-09 simplified abbrev: single argument;
2006-12-09 wenzelm 2006-12-09 TermSyntax.abbrev; ProofContext.set_expand_abbrevs;
2006-12-09 wenzelm 2006-12-09 added read/pretty_term_abbrev, print_abbrevs; tuned Consts signature; renamed expand_abbrevs to set_expand_abbrevs;
2006-12-09 wenzelm 2006-12-09 init_context: reset naming;
2006-12-09 wenzelm 2006-12-09 added 'print_abbrevs';
2006-12-09 wenzelm 2006-12-09 added print_abbrevs; exit: less verbosity;
2006-12-09 wenzelm 2006-12-09 added term_abbrev;
2006-12-09 wenzelm 2006-12-09 renamed reserved to reserved_names; added reserved: Name.context;
2006-12-09 wenzelm 2006-12-09 tuned Consts signature;
2006-12-09 wenzelm 2006-12-09 abbrevs: print original rhs;
2006-12-09 wenzelm 2006-12-09 abbreviate: always authentic, force expansion of internal abbreviations; tuned signature; tuned;
2006-12-09 wenzelm 2006-12-09 ML_Syntax.reserved(_names);
2006-12-09 wenzelm 2006-12-09 TermSyntax.abbrev;
2006-12-09 wenzelm 2006-12-09 added antiquotation abbrev;
2006-12-09 wenzelm 2006-12-09 added print_abbrevs;
2006-12-08 wenzelm 2006-12-08 tuned use_text; eval command line: skip over -q option;
2006-12-08 wenzelm 2006-12-08 added 'help' command (same of 'print_commands');
2006-12-08 wenzelm 2006-12-08 more careful evaluation of ML text, prevents spurious output;
2006-12-08 wenzelm 2006-12-08 date: forcing LC_ALL=C prevents funny file names;
2006-12-08 wenzelm 2006-12-08 root function: restore default interrupt handler; output file: avoid .exe (e.g. for Cygwin);
2006-12-08 paulson 2006-12-08 patched up the proofs agsin
2006-12-08 paulson 2006-12-08 removed use of put_name_hint, as the ATP linkup no longer needs this
2006-12-07 wenzelm 2006-12-07 reorganized structure Tactic vs. MetaSimplifier;
2006-12-07 wenzelm 2006-12-07 begin/end blocks; tuned notation;
2006-12-07 wenzelm 2006-12-07 abbrevs: more careful interpretation, avoid dynamic references to local names;
2006-12-07 wenzelm 2006-12-07 definition/abbreviation: single argument;
2006-12-07 wenzelm 2006-12-07 simplified add_abbrev -- single argument;
2006-12-07 wenzelm 2006-12-07 removed obsolete references to ProofGeneral/isa;
2006-12-07 wenzelm 2006-12-07 added input_mode;
2006-12-07 wenzelm 2006-12-07 tuned print_locale output; add_decls: Thm.internalK;
2006-12-07 wenzelm 2006-12-07 moved notation/abbrevs to TermSyntax;
2006-12-07 wenzelm 2006-12-07 expand_term: based on Envir.expand_term; tuned;
2006-12-07 wenzelm 2006-12-07 thms etc.: proper treatment of internal_fact with selection;
2006-12-07 wenzelm 2006-12-07 tuned pretty_src output;
2006-12-07 wenzelm 2006-12-07 simplified add_abbrevs: no mixfix;
2006-12-07 wenzelm 2006-12-07 added expand_term;
2006-12-07 wenzelm 2006-12-07 tuned;
2006-12-07 wenzelm 2006-12-07 Common term syntax declarations.
2006-12-07 wenzelm 2006-12-07 added Isar/term_syntax.ML;
2006-12-07 wenzelm 2006-12-07 TermSyntax.notation/abbrevs;
2006-12-07 paulson 2006-12-07 Removal of theorem tagging, which the ATP linkup no longer requires. Suffixes no longer blacklisted.
2006-12-07 paulson 2006-12-07 Removal of theorem tagging, which the ATP linkup no longer requires,
2006-12-07 wenzelm 2006-12-07 Poly/ML 5.0 setup for Isabelle2005.
2006-12-07 wenzelm 2006-12-07 reorganized structure Goal vs. Tactic;
2006-12-06 wenzelm 2006-12-06 export: added explicit term operation;
2006-12-06 wenzelm 2006-12-06 abbrevs: actually observe target_morphism;
2006-12-06 wenzelm 2006-12-06 added expand; export: added explicit term operation;
2006-12-06 wenzelm 2006-12-06 moved hidden_polymorphism to term.ML;
2006-12-06 wenzelm 2006-12-06 added hidden_polymorphism (from variable.ML);
2006-12-06 wenzelm 2006-12-06 add_abbrevs: moved common parts to consts.ML;
2006-12-06 wenzelm 2006-12-06 abbreviate: improved error handling, return result;
2006-12-06 wenzelm 2006-12-06 export: added explicit term operation; tuned export_morphism -- lean closure;
2006-12-06 wenzelm 2006-12-06 LocalDefs.expand;
2006-12-06 paulson 2006-12-06 Improved tracing
2006-12-06 wenzelm 2006-12-06 no timing;
2006-12-06 wenzelm 2006-12-06 simplified ML bindings;
2006-12-06 wenzelm 2006-12-06 simplified ML bindings -- moved to HOL.thy; removed confusing simpset_basic/simplify;
2006-12-06 wenzelm 2006-12-06 added basic ML bindings;