2005-09-28 |
wenzelm |
revert 'defs' advertisement;
|
file |
diff |
annotate
|
2005-09-27 |
wenzelm |
more details about incomplete 'defs';
|
file |
diff |
annotate
|
2005-09-27 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
2005-09-27 |
berghofe |
Added entries for code_module, code_library, and value.
|
file |
diff |
annotate
|
2005-09-25 |
wenzelm |
* Hyperreal: A theory of Taylor series.
|
file |
diff |
annotate
|
2005-09-23 |
webertj |
new sat tactic
|
file |
diff |
annotate
|
2005-09-23 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
2005-09-23 |
paulson |
ATP linkup
|
file |
diff |
annotate
|
2005-09-22 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
2005-09-22 |
huffman |
HOLCF theorem naming conventions
|
file |
diff |
annotate
|
2005-09-21 |
haftmann |
added AList.make, eq_fst, apr ...
|
file |
diff |
annotate
|
2005-09-21 |
wenzelm |
tunes;
|
file |
diff |
annotate
|
2005-09-20 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
2005-09-20 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
2005-09-20 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
2005-09-20 |
wenzelm |
HOL/ex/Chinese.thy;
|
file |
diff |
annotate
|
2005-09-20 |
haftmann |
infix operator precedence
|
file |
diff |
annotate
|
2005-09-17 |
wenzelm |
HTML.with_charset;
|
file |
diff |
annotate
|
2005-09-17 |
wenzelm |
Cube: converted to Isar, use locales;
|
file |
diff |
annotate
|
2005-09-16 |
huffman |
add HOLCF entries for pcpodef, cont_proc, fixrec;
|
file |
diff |
annotate
|
2005-09-16 |
ballarin |
tuned
|
file |
diff |
annotate
|
2005-09-15 |
wenzelm |
* Improved efficiency of the Simplifier etc.;
|
file |
diff |
annotate
|
2005-09-15 |
wenzelm |
incorporated HOL/Hyperreal/CHANGES;
|
file |
diff |
annotate
|
2005-09-15 |
wenzelm |
command 'thms_containing' has been discontinued in favour of 'find_theorems';
|
file |
diff |
annotate
|
2005-09-15 |
haftmann |
AList, the_*
|
file |
diff |
annotate
|
2005-09-14 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
2005-09-14 |
wenzelm |
hide: added option '(open)';
|
file |
diff |
annotate
|
2005-09-14 |
schirmer |
... prem19
|
file |
diff |
annotate
|
2005-09-14 |
wenzelm |
Method comm_ring for proving equalities in commutative rings.
|
file |
diff |
annotate
|
2005-09-14 |
wenzelm |
HOL: method comm_ring;
|
file |
diff |
annotate
|
2005-09-13 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
2005-09-06 |
wenzelm |
axclass: name space prefix is now "c_class" instead of just "c";
|
file |
diff |
annotate
|
2005-09-05 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
2005-09-05 |
wenzelm |
Markup commands 'chapter' .. 'text' support optional locale specification;
|
file |
diff |
annotate
|
2005-09-02 |
ballarin |
print_locale omits facts by default
|
file |
diff |
annotate
|
2005-08-31 |
wenzelm |
* Delimiters of outer tokens now produce separate LaTeX macros;
|
file |
diff |
annotate
|
2005-08-30 |
paulson |
patterns in setsum and setprod
|
file |
diff |
annotate
|
2005-08-28 |
wenzelm |
* ML functions legacy_bindings and use_legacy_bindings;
|
file |
diff |
annotate
|
2005-08-28 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
2005-08-24 |
ballarin |
Printing of interpretations: option to show witness theorems;
|
file |
diff |
annotate
|
2005-08-18 |
wenzelm |
* The ML antiquotation prints type-checked ML expressions verbatim.
|
file |
diff |
annotate
|
2005-08-18 |
wenzelm |
* Proper output of proof terms within a proof context;
|
file |
diff |
annotate
|
2005-08-17 |
ballarin |
Interpretation in locales.
|
file |
diff |
annotate
|
2005-08-17 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
2005-08-16 |
wenzelm |
* Command tags control specific markup of certain regions of text (replaces usedir -H);
|
file |
diff |
annotate
|
2005-08-03 |
avigad |
mentioned change to exp_ge_add_one_self, new transitivity rules
|
file |
diff |
annotate
|
2005-08-01 |
wenzelm |
* Pure/Simplifier: improved handling of bound variables;
|
file |
diff |
annotate
|
2005-07-29 |
avigad |
mentioned Ln in NEWS
|
file |
diff |
annotate
|
2005-07-28 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
2005-07-25 |
avigad |
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
|
file |
diff |
annotate
|
2005-07-19 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
2005-07-19 |
avigad |
added list of theorem changes to NEWS
|
file |
diff |
annotate
|
2005-07-18 |
haftmann |
reverted from fold_yield to fold_map
|
file |
diff |
annotate
|
2005-07-15 |
wenzelm |
*** empty log message ***
|
file |
diff |
annotate
|
2005-07-15 |
wenzelm |
* Pure/library.ML: several combinators for linear functional transformations;
|
file |
diff |
annotate
|
2005-07-14 |
wenzelm |
* Improved 'oracle' command -- type-safe;
|
file |
diff |
annotate
|
2005-07-13 |
wenzelm |
* Isar session: The initial use of ROOT.ML is now always timed;
|
file |
diff |
annotate
|
2005-07-06 |
wenzelm |
* Pure: Output.time_accumulator;
|
file |
diff |
annotate
|
2005-07-06 |
wenzelm |
isatool fixheaders;
|
file |
diff |
annotate
|
2005-07-05 |
wenzelm |
tuned;
|
file |
diff |
annotate
|