| 2007-10-17 |
wenzelm |
removed obsolete unlocalize_mfix;
|
changeset |
files
|
| 2007-10-17 |
wenzelm |
removed obsolete unlocalize_mixfix;
|
changeset |
files
|
| 2007-10-17 |
wenzelm |
locale pred: authentic syntax, tuned aprop_tr' accordingly;
|
changeset |
files
|
| 2007-10-17 |
wenzelm |
store external accesses within name space (as produced by naming policy);
|
changeset |
files
|
| 2007-10-17 |
wenzelm |
removed unused set_policy;
|
changeset |
files
|
| 2007-10-17 |
wenzelm |
replaced NameSpace.accesses' by NameSpace.external_names (depening on naming);
|
changeset |
files
|
| 2007-10-17 |
nipkow |
added sorted_list_of_set
|
changeset |
files
|
| 2007-10-17 |
wenzelm |
tuned fork_mixfix (back from class.ML);
|
changeset |
files
|
| 2007-10-17 |
wenzelm |
clarified naming conventions of 'parse' and 'check' (as opposed to former 'cert');
|
changeset |
files
|
| 2007-10-17 |
wenzelm |
removed obsolete fork_mixfix (back to theory_target.ML);
|
changeset |
files
|
| 2007-10-17 |
wenzelm |
updated;
|
changeset |
files
|
| 2007-10-16 |
haftmann |
clarified fork_mixfix
|
changeset |
files
|
| 2007-10-16 |
haftmann |
exported standard_term_check
|
changeset |
files
|
| 2007-10-16 |
haftmann |
global class syntax
|
changeset |
files
|
| 2007-10-16 |
haftmann |
added yield_singleton
|
changeset |
files
|
| 2007-10-16 |
wenzelm |
Syntax.(un)check: explicit result option;
|
changeset |
files
|
| 2007-10-16 |
wenzelm |
apply_wrappers: perhaps_apply/loop;
|
changeset |
files
|
| 2007-10-16 |
wenzelm |
added perhaps_apply/loop;
|
changeset |
files
|
| 2007-10-16 |
wenzelm |
Mark A. Hillebrand, DFKI: Robust sub/superscripts in LaTeX document output.
|
changeset |
files
|
| 2007-10-16 |
wenzelm |
updated;
|
changeset |
files
|
| 2007-10-16 |
wenzelm |
DeclareRobustCommand isascriptstyle (enables sub/superscripts within section headings etc.);
|
changeset |
files
|
| 2007-10-16 |
wenzelm |
tuned Const.the_abbreviation;
|
changeset |
files
|
| 2007-10-16 |
wenzelm |
misc cleanup of abbrev/local_const;
|
changeset |
files
|
| 2007-10-16 |
wenzelm |
added revert_abbrev;
|
changeset |
files
|
| 2007-10-16 |
wenzelm |
add_bind: close_schematic_term;
|
changeset |
files
|
| 2007-10-16 |
wenzelm |
tuned hidden_polymorphism;
|
changeset |
files
|
| 2007-10-16 |
wenzelm |
add_abbrev: removed Logic.legacy_varifyT, do not unvarify result (again);
|
changeset |
files
|
| 2007-10-16 |
wenzelm |
the_abbreviation: return plain rhs only;
|
changeset |
files
|
| 2007-10-16 |
paulson |
added the "max_sledgehammers" option
|
changeset |
files
|
| 2007-10-16 |
krauss |
Fixed variable naming in mutual induction rules
|
changeset |
files
|
| 2007-10-16 |
krauss |
"sequential" is no longer a keyword. It is still used as before, but as a normal
|
changeset |
files
|
| 2007-10-16 |
urbanc |
polished some comments
|
changeset |
files
|
| 2007-10-15 |
wenzelm |
unparse_arity: unparse type constructor as well;
|
changeset |
files
|
| 2007-10-15 |
wenzelm |
renamed Consts.the_declaration to Consts.the_type;
|
changeset |
files
|
| 2007-10-15 |
wenzelm |
renamed the_declaration to the_type;
|
changeset |
files
|
| 2007-10-15 |
haftmann |
tuned
|
changeset |
files
|
| 2007-10-15 |
haftmann |
swapped constant components
|
changeset |
files
|
| 2007-10-15 |
haftmann |
canonical interpretation interface
|
changeset |
files
|
| 2007-10-15 |
haftmann |
prefer first constant component on merge
|
changeset |
files
|
| 2007-10-15 |
haftmann |
explicit parameter for class finite
|
changeset |
files
|
| 2007-10-15 |
wenzelm |
tuned comment;
|
changeset |
files
|
| 2007-10-15 |
wenzelm |
more on authentic syntax;
|
changeset |
files
|
| 2007-10-15 |
wenzelm |
updated method "ferrack";
|
changeset |
files
|
| 2007-10-14 |
webertj |
interpreter for List.append added again
|
changeset |
files
|
| 2007-10-14 |
webertj |
quick_and_dirty (again) not touched anymore
|
changeset |
files
|
| 2007-10-14 |
wenzelm |
require_thy: read_text *after* checking parents
|
changeset |
files
|
| 2007-10-14 |
wenzelm |
gen_add_inductive_i: treat abbrevs as local defs, expand by export;
|
changeset |
files
|
| 2007-10-13 |
wenzelm |
tuned various Class interfaces;
|
changeset |
files
|
| 2007-10-13 |
wenzelm |
removed obsolete Class.class_of_locale/locale_of_class;
|
changeset |
files
|
| 2007-10-13 |
wenzelm |
tuned;
|
changeset |
files
|
| 2007-10-13 |
wenzelm |
added add_def;
|
changeset |
files
|
| 2007-10-13 |
wenzelm |
added is_class;
|
changeset |
files
|
| 2007-10-13 |
wenzelm |
PolyML.Compiler.maxInlineSize := 80;
|
changeset |
files
|
| 2007-10-13 |
wenzelm |
abbrev: return hypothetical def;
|
changeset |
files
|
| 2007-10-13 |
wenzelm |
renamed def to define;
|
changeset |
files
|
| 2007-10-13 |
wenzelm |
(un)overload: full rewrite;
|
changeset |
files
|
| 2007-10-13 |
wenzelm |
add_abbrevs: unvarify result;
|
changeset |
files
|
| 2007-10-13 |
wenzelm |
replaced obsolete Theory.add_finals_i by Theory.add_deps;
|
changeset |
files
|
| 2007-10-13 |
wenzelm |
Theory.specify_const: added deps argument;
|
changeset |
files
|
| 2007-10-13 |
wenzelm |
renamed LocalTheory.def to LocalTheory.define;
|
changeset |
files
|