| 2005-10-31 |
haftmann |
2005-10-31 |
nth_*, fold_index refined
|
file | diff | annotate |
| 2005-10-28 |
wenzelm |
2005-10-28 |
tuned;
|
file | diff | annotate |
| 2005-10-28 |
wenzelm |
2005-10-28 |
* Pure/Isar: literal facts;
* ML/Pure: tuned Thm.lift_rule;
* ML/Pure: renamed Goal constant to prop, more general uses;
|
file | diff | annotate |
| 2005-10-27 |
wenzelm |
2005-10-27 |
* HOL: alternative iff syntax;
|
file | diff | annotate |
| 2005-10-27 |
haftmann |
2005-10-27 |
added module Pure/General/rat.ML
|
file | diff | annotate |
| 2005-10-21 |
wenzelm |
2005-10-21 |
* Legacy goal package: reduced interface to the bare minimum required to keep existing proof scripts running.
* Internal goals: structure Goal.
|
file | diff | annotate |
| 2005-10-19 |
wenzelm |
2005-10-19 |
* Theory syntax: discontinued non-Isar format and old Isar headers;
|
file | diff | annotate |
| 2005-10-18 |
wenzelm |
2005-10-18 |
Simplifier.context/theory_context;
|
file | diff | annotate |
| 2005-10-17 |
wenzelm |
2005-10-17 |
* Simplifier: simpset of a running simplification process contains a proof context;
* Simplifier.inherit_context supercedes Simplifier.inherit_bounds;
* Simplifier/Classical Reasoner: more abstract interfaces change_simpset/claset;
|
file | diff | annotate |
| 2005-10-17 |
wenzelm |
2005-10-17 |
tuned;
|
file | diff | annotate |
| 2005-10-15 |
wenzelm |
2005-10-15 |
tuned;
|
file | diff | annotate |
| 2005-10-15 |
wenzelm |
2005-10-15 |
* antiquotations ML_type, ML_struct;
* Isar 'guess' element;
|
file | diff | annotate |
| 2005-10-09 |
webertj |
2005-10-09 |
Tactics sat and satx reimplemented, several improvements
|
file | diff | annotate |
| 2005-10-08 |
nipkow |
2005-10-08 |
*** empty log message ***
|
file | diff | annotate |
| 2005-10-07 |
wenzelm |
2005-10-07 |
tuned;
|
file | diff | annotate |
| 2005-10-07 |
wenzelm |
2005-10-07 |
added dummy variable binding;
removed obsolete _K;
|
file | diff | annotate |
| 2005-10-04 |
wenzelm |
2005-10-04 |
* Command 'find_theorems': support * wildcard in name: criterion.
|
file | diff | annotate |
| 2005-09-29 |
wenzelm |
2005-09-29 |
pdfsetup.sty: better not rely on ifpdf.sty;
|
file | diff | annotate |
| 2005-09-29 |
wenzelm |
2005-09-29 |
Isabelle2005 (October 2005);
pdfsetup.sty now requires ifpdf.sty;
added Simplifier.debug_bounds;
do not advertize Simplifier.add_context_simprocs etc., which are to be replaced soon;
|
file | diff | annotate |
| 2005-09-29 |
wenzelm |
2005-09-29 |
tuned;
|
file | diff | annotate |
| 2005-09-28 |
webertj |
2005-09-28 |
pointer to HOL/ex/SAT_Examples.thy added
|
file | diff | annotate |
| 2005-09-28 |
wenzelm |
2005-09-28 |
revert 'defs' advertisement;
removed PG/xemacs note, which is actually wrong now;
tuned;
|
file | diff | annotate |
| 2005-09-27 |
wenzelm |
2005-09-27 |
more details about incomplete 'defs';
|
file | diff | annotate |
| 2005-09-27 |
wenzelm |
2005-09-27 |
tuned;
|
file | diff | annotate |
| 2005-09-27 |
berghofe |
2005-09-27 |
Added entries for code_module, code_library, and value.
|
file | diff | annotate |
| 2005-09-25 |
wenzelm |
2005-09-25 |
* Hyperreal: A theory of Taylor series.
|
file | diff | annotate |
| 2005-09-23 |
webertj |
2005-09-23 |
new sat tactic
|
file | diff | annotate |
| 2005-09-23 |
wenzelm |
2005-09-23 |
tuned;
|
file | diff | annotate |
| 2005-09-23 |
paulson |
2005-09-23 |
ATP linkup
|
file | diff | annotate |
| 2005-09-23 |
nipkow |
2005-09-23 |
*** empty log message ***
|
file | diff | annotate |
| 2005-09-22 |
huffman |
2005-09-22 |
HOLCF theorem naming conventions
|
file | diff | annotate |
| 2005-09-21 |
haftmann |
2005-09-21 |
added AList.make, eq_fst, apr ...
|
file | diff | annotate |
| 2005-09-21 |
wenzelm |
2005-09-21 |
tunes;
|
file | diff | annotate |
| 2005-09-21 |
wenzelm |
2005-09-21 |
tuned;
|
file | diff | annotate |
| 2005-09-20 |
wenzelm |
2005-09-20 |
tuned;
|
file | diff | annotate |
| 2005-09-20 |
wenzelm |
2005-09-20 |
tuned;
|
file | diff | annotate |
| 2005-09-20 |
wenzelm |
2005-09-20 |
HOL/ex/Chinese.thy;
PROOFGENERAL_OPTIONS: no longer prefer xemacs;
|
file | diff | annotate |
| 2005-09-20 |
haftmann |
2005-09-20 |
infix operator precedence
|
file | diff | annotate |
| 2005-09-17 |
wenzelm |
2005-09-17 |
HTML.with_charset;
|
file | diff | annotate |
| 2005-09-17 |
wenzelm |
2005-09-17 |
Cube: converted to Isar, use locales;
|
file | diff | annotate |
| 2005-09-16 |
huffman |
2005-09-16 |
add HOLCF entries for pcpodef, cont_proc, fixrec;
add HOL-Complex entry for transfer tactic;
clean up lists of theories in HOL-Complex entries
|
file | diff | annotate |
| 2005-09-16 |
ballarin |
2005-09-16 |
tuned
|
file | diff | annotate |
| 2005-09-15 |
wenzelm |
2005-09-15 |
* Improved efficiency of the Simplifier etc.;
|
file | diff | annotate |
| 2005-09-15 |
wenzelm |
2005-09-15 |
incorporated HOL/Hyperreal/CHANGES;
|
file | diff | annotate |
| 2005-09-15 |
wenzelm |
2005-09-15 |
command 'thms_containing' has been discontinued in favour of 'find_theorems';
TableFun/Symtab: curried lookup and update;
tuned;
|
file | diff | annotate |
| 2005-09-15 |
haftmann |
2005-09-15 |
AList, the_*
|
file | diff | annotate |
| 2005-09-14 |
wenzelm |
2005-09-14 |
tuned;
|
file | diff | annotate |
| 2005-09-14 |
wenzelm |
2005-09-14 |
hide: added option '(open)';
|
file | diff | annotate |
| 2005-09-14 |
schirmer |
2005-09-14 |
... prem19
|
file | diff | annotate |
| 2005-09-14 |
wenzelm |
2005-09-14 |
Method comm_ring for proving equalities in commutative rings.
|
file | diff | annotate |
| 2005-09-14 |
wenzelm |
2005-09-14 |
HOL: method comm_ring;
Proof General: Unicode (UTF-8) support;
|
file | diff | annotate |
| 2005-09-13 |
wenzelm |
2005-09-13 |
tuned;
|
file | diff | annotate |
| 2005-09-06 |
wenzelm |
2005-09-06 |
axclass: name space prefix is now "c_class" instead of just "c";
typedef: proper support for polymorphic sets;
|
file | diff | annotate |
| 2005-09-05 |
wenzelm |
2005-09-05 |
tuned;
|
file | diff | annotate |
| 2005-09-05 |
wenzelm |
2005-09-05 |
Markup commands 'chapter' .. 'text' support optional locale specification;
|
file | diff | annotate |
| 2005-09-02 |
ballarin |
2005-09-02 |
print_locale omits facts by default
|
file | diff | annotate |
| 2005-08-31 |
wenzelm |
2005-08-31 |
* Delimiters of outer tokens now produce separate LaTeX macros;
* isatool usedir: option -C (default true) controls copying of document directory;
|
file | diff | annotate |
| 2005-08-30 |
paulson |
2005-08-30 |
patterns in setsum and setprod
|
file | diff | annotate |
| 2005-08-28 |
wenzelm |
2005-08-28 |
* ML functions legacy_bindings and use_legacy_bindings;
|
file | diff | annotate |
| 2005-08-28 |
wenzelm |
2005-08-28 |
tuned;
|
file | diff | annotate |