2006-12-09 ago wenzelm abbrevs: print original rhs;
2006-12-09 ago wenzelm abbreviate: always authentic, force expansion of internal abbreviations;
2006-12-09 ago wenzelm ML_Syntax.reserved(_names);
2006-12-09 ago wenzelm TermSyntax.abbrev;
2006-12-09 ago wenzelm added antiquotation abbrev;
2006-12-09 ago wenzelm added print_abbrevs;
2006-12-08 ago wenzelm tuned use_text;
2006-12-08 ago wenzelm added 'help' command (same of 'print_commands');
2006-12-08 ago wenzelm more careful evaluation of ML text, prevents spurious output;
2006-12-08 ago wenzelm date: forcing LC_ALL=C prevents funny file names;
2006-12-08 ago wenzelm root function: restore default interrupt handler;
2006-12-08 ago paulson patched up the proofs agsin
2006-12-08 ago paulson removed use of put_name_hint, as the ATP linkup no longer needs this
2006-12-07 ago wenzelm reorganized structure Tactic vs. MetaSimplifier;
2006-12-07 ago wenzelm begin/end blocks;
2006-12-07 ago wenzelm abbrevs: more careful interpretation, avoid dynamic references to local names;
2006-12-07 ago wenzelm definition/abbreviation: single argument;
2006-12-07 ago wenzelm simplified add_abbrev -- single argument;
2006-12-07 ago wenzelm removed obsolete references to ProofGeneral/isa;
2006-12-07 ago wenzelm added input_mode;
2006-12-07 ago wenzelm tuned print_locale output;
2006-12-07 ago wenzelm moved notation/abbrevs to TermSyntax;
2006-12-07 ago wenzelm expand_term: based on Envir.expand_term;
2006-12-07 ago wenzelm thms etc.: proper treatment of internal_fact with selection;
2006-12-07 ago wenzelm tuned pretty_src output;
2006-12-07 ago wenzelm simplified add_abbrevs: no mixfix;
2006-12-07 ago wenzelm added expand_term;
2006-12-07 ago wenzelm tuned;
2006-12-07 ago wenzelm Common term syntax declarations.
2006-12-07 ago wenzelm added Isar/term_syntax.ML;
2006-12-07 ago wenzelm TermSyntax.notation/abbrevs;
2006-12-07 ago paulson Removal of theorem tagging, which the ATP linkup no longer requires.
2006-12-07 ago paulson Removal of theorem tagging, which the ATP linkup no longer requires,
2006-12-07 ago wenzelm Poly/ML 5.0 setup for Isabelle2005.
2006-12-07 ago wenzelm reorganized structure Goal vs. Tactic;
2006-12-06 ago wenzelm export: added explicit term operation;
2006-12-06 ago wenzelm abbrevs: actually observe target_morphism;
2006-12-06 ago wenzelm added expand;
2006-12-06 ago wenzelm moved hidden_polymorphism to term.ML;
2006-12-06 ago wenzelm added hidden_polymorphism (from variable.ML);
2006-12-06 ago wenzelm add_abbrevs: moved common parts to consts.ML;
2006-12-06 ago wenzelm abbreviate: improved error handling, return result;
2006-12-06 ago wenzelm export: added explicit term operation;
2006-12-06 ago wenzelm LocalDefs.expand;
2006-12-06 ago paulson Improved tracing
2006-12-06 ago wenzelm no timing;
2006-12-06 ago wenzelm simplified ML bindings;
2006-12-06 ago wenzelm simplified ML bindings -- moved to HOL.thy;
2006-12-06 ago wenzelm added basic ML bindings;
2006-12-06 ago wenzelm added aliases for nat_recs/cases;
2006-12-06 ago wenzelm removed legacy ML bindings;
2006-12-06 ago wenzelm reduced to genuine legacy bindings -- others in HOL.thy;
2006-12-06 ago wenzelm removed legacy ML bindings;
2006-12-05 ago wenzelm target_name: allow qualified names;
2006-12-05 ago wenzelm add_notation: permissive about undeclared consts;
2006-12-05 ago wenzelm generic_goal: enable stmt mode;
2006-12-05 ago wenzelm encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
2006-12-05 ago wenzelm notation/abbreviation: more serious handling of morphisms;
2006-12-05 ago wenzelm print_syntax etc.: plain Toplevel.context_of;
2006-12-05 ago wenzelm attribute value: morphism;