2007-10-16 wenzelm 2007-10-16 Mark A. Hillebrand, DFKI: Robust sub/superscripts in LaTeX document output.
2007-10-16 wenzelm 2007-10-16 updated;
2007-10-16 wenzelm 2007-10-16 DeclareRobustCommand isascriptstyle (enables sub/superscripts within section headings etc.);
2007-10-16 wenzelm 2007-10-16 tuned Const.the_abbreviation;
2007-10-16 wenzelm 2007-10-16 misc cleanup of abbrev/local_const;
2007-10-16 wenzelm 2007-10-16 added revert_abbrev; contract_abbrevs: ignore Syntax.internalM (changed meaning of this special case); print_abbrevs: proper treatment of global consts (after local/global swap);
2007-10-16 wenzelm 2007-10-16 add_bind: close_schematic_term;
2007-10-16 wenzelm 2007-10-16 tuned hidden_polymorphism; added close_schematic_term;
2007-10-16 wenzelm 2007-10-16 add_abbrev: removed Logic.legacy_varifyT, do not unvarify result (again); added revert_abbrev;
2007-10-16 wenzelm 2007-10-16 the_abbreviation: return plain rhs only; force_expand: expand to plain rhs; added revert_abbrev; tuned;
2007-10-16 paulson 2007-10-16 added the "max_sledgehammers" option
2007-10-16 krauss 2007-10-16 Fixed variable naming in mutual induction rules
2007-10-16 krauss 2007-10-16 "sequential" is no longer a keyword. It is still used as before, but as a normal identifier => no pollution of keyword space
2007-10-16 urbanc 2007-10-16 polished some comments
2007-10-15 wenzelm 2007-10-15 unparse_arity: unparse type constructor as well;
2007-10-15 wenzelm 2007-10-15 renamed Consts.the_declaration to Consts.the_type;
2007-10-15 wenzelm 2007-10-15 renamed the_declaration to the_type; added type_scheme, which covers proper consts and abbreviations (like typargs); tuned;
2007-10-15 haftmann 2007-10-15 tuned
2007-10-15 haftmann 2007-10-15 swapped constant components
2007-10-15 haftmann 2007-10-15 canonical interpretation interface
2007-10-15 haftmann 2007-10-15 prefer first constant component on merge
2007-10-15 haftmann 2007-10-15 explicit parameter for class finite
2007-10-15 wenzelm 2007-10-15 tuned comment;
2007-10-15 wenzelm 2007-10-15 more on authentic syntax;
2007-10-15 wenzelm 2007-10-15 updated method "ferrack";
2007-10-15 webertj 2007-10-15 interpreter for List.append added again
2007-10-15 webertj 2007-10-15 quick_and_dirty (again) not touched anymore
2007-10-14 wenzelm 2007-10-14 require_thy: read_text *after* checking parents (otherwise outdating an existing descendant will leave the dependencies corrupted);
2007-10-14 wenzelm 2007-10-14 gen_add_inductive_i: treat abbrevs as local defs, expand by export; tuned;
2007-10-14 wenzelm 2007-10-14 tuned various Class interfaces; tuned;
2007-10-14 wenzelm 2007-10-14 removed obsolete Class.class_of_locale/locale_of_class;
2007-10-14 wenzelm 2007-10-14 tuned;
2007-10-14 wenzelm 2007-10-14 added add_def;
2007-10-14 wenzelm 2007-10-14 added is_class; tuned signature of add_const/abbrev_in_class; removed obsolete class_of_locale/locale_of_class; tuned name prefixing: Sign.full_name does the job;
2007-10-13 wenzelm 2007-10-13 PolyML.Compiler.maxInlineSize := 80;
2007-10-13 wenzelm 2007-10-13 abbrev: return hypothetical def; replaced obsolete Theory.add_finals_i by Theory.add_deps; misc cleanup;
2007-10-13 wenzelm 2007-10-13 renamed def to define; abbrev: return hypothetical def;
2007-10-13 wenzelm 2007-10-13 (un)overload: full rewrite; use Attrib.attribute_i for internal args; misc tuning;
2007-10-13 wenzelm 2007-10-13 add_abbrevs: unvarify result;
2007-10-13 wenzelm 2007-10-13 replaced obsolete Theory.add_finals_i by Theory.add_deps;
2007-10-13 wenzelm 2007-10-13 Theory.specify_const: added deps argument;
2007-10-13 wenzelm 2007-10-13 renamed LocalTheory.def to LocalTheory.define;
2007-10-12 webertj 2007-10-12 typo in comment fixed
2007-10-12 webertj 2007-10-12 significant code overhaul, bugfix for inductive data types
2007-10-12 wenzelm 2007-10-12 added generic provide_file; tuned;
2007-10-12 wenzelm 2007-10-12 pass explicit target record -- more informative peek operation; removed obsolete hide_abbrev; misc tuning;
2007-10-12 wenzelm 2007-10-12 more informative TheoryTarget.peek operation;
2007-10-12 wenzelm 2007-10-12 fork_mixfix: explicit bool argument;
2007-10-12 wenzelm 2007-10-12 eval_term: moved actual evaluation out of CRITICAL section;
2007-10-12 paulson 2007-10-12 preventing eta-redexes in theorems from causing failure
2007-10-12 paulson 2007-10-12 trying to make it run faster
2007-10-12 paulson 2007-10-12 calling the correct interface
2007-10-12 wenzelm 2007-10-12 replaced syntax/translations by abbreviation;
2007-10-12 haftmann 2007-10-12 updated
2007-10-12 haftmann 2007-10-12 dropped local_syntax
2007-10-12 haftmann 2007-10-12 tuned
2007-10-12 haftmann 2007-10-12 (intermediate quickfix)
2007-10-12 haftmann 2007-10-12 removed
2007-10-12 haftmann 2007-10-12 added
2007-10-12 paulson 2007-10-12 metis calls