| 2006-06-15 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| 2006-06-12 |
berghofe |
Added "evaluation" method.
|
file |
diff |
annotate
|
| 2006-06-07 |
wenzelm |
* Theory syntax: some popular names (e.g. "class", "if") are now keywords.
|
file |
diff |
annotate
|
| 2006-06-06 |
ballarin |
Improved parameter management of locales.
|
file |
diff |
annotate
|
| 2006-05-24 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2006-05-24 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2006-05-24 |
wenzelm |
Pure: update on overloaded defs;
|
file |
diff |
annotate
|
| 2006-05-17 |
wenzelm |
* Pure: syntax 'CONST name' produces a fully internalized constant;
|
file |
diff |
annotate
|
| 2006-05-16 |
wenzelm |
* Isar/locale: 'const_syntax';
|
file |
diff |
annotate
|
| 2006-05-16 |
wenzelm |
* Pure/library: divide_and_conquer;
|
file |
diff |
annotate
|
| 2006-05-13 |
wenzelm |
* Pure: overloaded definitions are now actually checked for acyclic dependencies;
|
file |
diff |
annotate
|
| 2006-05-06 |
wenzelm |
* Isar: removed obsolete 'concl is' patterns.
|
file |
diff |
annotate
|
| 2006-05-05 |
wenzelm |
* Library: theory Accessible_Part has been move to main HOL.
|
file |
diff |
annotate
|
| 2006-04-30 |
wenzelm |
* Pure: axclasses now purely definitional;
|
file |
diff |
annotate
|
| 2006-04-09 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| 2006-04-08 |
wenzelm |
refined 'abbreviation';
|
file |
diff |
annotate
|
| 2006-03-17 |
ballarin |
Renamed setsum_mult to setsum_right_distrib.
|
file |
diff |
annotate
|
| 2006-03-17 |
haftmann |
renamed op < <= to Orderings.less(_eq)
|
file |
diff |
annotate
|
| 2006-03-14 |
wenzelm |
print_statement;
|
file |
diff |
annotate
|
| 2006-03-14 |
wenzelm |
Pure: no_translations;
|
file |
diff |
annotate
|
| 2006-03-13 |
schirmer |
entry for Library/AssocList
|
file |
diff |
annotate
|
| 2006-03-10 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2006-03-10 |
haftmann |
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
|
file |
diff |
annotate
|
| 2006-03-08 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2006-03-08 |
wenzelm |
Isar/method: goal restriction;
|
file |
diff |
annotate
|
| 2006-03-08 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| 2006-02-16 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2006-02-16 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2006-02-16 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2006-02-16 |
wenzelm |
* Isar/locales: new derived specification elements 'definition', 'abbreviation', 'axiomatization';
|
file |
diff |
annotate
|
| 2006-02-12 |
wenzelm |
* ML/Pure/General: improved join interface for tables;
|
file |
diff |
annotate
|
| 2006-02-12 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2006-02-10 |
wenzelm |
* ML/Pure: generic Args/Attrib syntax everywhere;
|
file |
diff |
annotate
|
| 2006-02-08 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| 2006-02-02 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2006-02-02 |
wenzelm |
* Isar: 'obtains' element;
|
file |
diff |
annotate
|
| 2006-01-30 |
wenzelm |
* Pure: 'advanced' translation functions use Context.generic instead of just theory;
|
file |
diff |
annotate
|
| 2006-01-28 |
wenzelm |
Pure/Isar: (un)folded, (un)fold, unfolding support
|
file |
diff |
annotate
|
| 2006-01-21 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2006-01-21 |
wenzelm |
* ML: simplified type attribute;
|
file |
diff |
annotate
|
| 2006-01-19 |
wenzelm |
* ML/Isar: theory setup has type (theory -> theory);
|
file |
diff |
annotate
|
| 2006-01-15 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2006-01-15 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2006-01-15 |
wenzelm |
* Classical: optional weight for attributes;
|
file |
diff |
annotate
|
| 2006-01-14 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2006-01-14 |
wenzelm |
* ML/Isar: simplified treatment of user-level errors;
|
file |
diff |
annotate
|
| 2006-01-13 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| 2006-01-10 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2006-01-10 |
wenzelm |
* ML: generic context, data, attributes;
|
file |
diff |
annotate
|
| 2006-01-07 |
wenzelm |
* Provers/induct: improved simultaneous goals -- nested cases;
|
file |
diff |
annotate
|
| 2006-01-06 |
wenzelm |
Pure/Isar: Toplevel.theory_to_proof admits transactions that modify the theory;
|
file |
diff |
annotate
|
| 2006-01-04 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2006-01-04 |
wenzelm |
* Pure/Isar: Toplevel.theory_theory_to_proof;
|
file |
diff |
annotate
|
| 2006-01-03 |
paulson |
Provers/classical: stricter checks to ensure that supplied intro, dest and
|
file |
diff |
annotate
|
| 2006-01-03 |
haftmann |
rearranged burrow_split to fold_burrow to allow composition with fold_map
|
file |
diff |
annotate
|
| 2006-01-02 |
wenzelm |
* Pure/Isar: new command 'unfolding';
|
file |
diff |
annotate
|
| 2005-12-31 |
wenzelm |
* Provers/classical: removed obsolete classical version of elim_format;
|
file |
diff |
annotate
|
| 2005-12-23 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2005-12-23 |
wenzelm |
* Provers/induct: support simultaneous goals with mutual rules;
|
file |
diff |
annotate
|
| 2005-12-23 |
haftmann |
is_prefix
|
file |
diff |
annotate
|