2006-01-03 |
wenzelm |
2006-01-03 |
* Pure/Isar: new command 'unfolding';
* ML/Provers: more generic wrt. syntax of object-logics;
tuned;
|
file | diff | annotate |
2005-12-31 |
wenzelm |
2005-12-31 |
* Provers/classical: removed obsolete classical version of elim_format;
|
file | diff | annotate |
2005-12-23 |
wenzelm |
2005-12-23 |
tuned;
|
file | diff | annotate |
2005-12-23 |
wenzelm |
2005-12-23 |
* Provers/induct: support simultaneous goals with mutual rules;
|
file | diff | annotate |
2005-12-23 |
haftmann |
2005-12-23 |
is_prefix
|
file | diff | annotate |
2005-12-22 |
wenzelm |
2005-12-22 |
tuned;
|
file | diff | annotate |
2005-12-22 |
wenzelm |
2005-12-22 |
* induct: improved treatment of mutual goals and mutual rules;
|
file | diff | annotate |
2005-12-21 |
haftmann |
2005-12-21 |
discontinued unflat in favour of burrow and burrow_split
|
file | diff | annotate |
2005-12-20 |
wenzelm |
2005-12-20 |
tuned;
|
file | diff | annotate |
2005-12-16 |
haftmann |
2005-12-16 |
re-arranged tuples (theory * 'a) to ('a * theory) in Pure
|
file | diff | annotate |
2005-12-13 |
wenzelm |
2005-12-13 |
Provers/induct: coinduct;
HOL/Library: theory Coinductive_List;
|
file | diff | annotate |
2005-12-08 |
wenzelm |
2005-12-08 |
removed hint for Classical.swap, which is not really user-level anyway;
|
file | diff | annotate |
2005-12-08 |
wenzelm |
2005-12-08 |
* HOL: Theorem 'swap' is no longer bound at the ML top-level.
|
file | diff | annotate |
2005-11-30 |
wenzelm |
2005-11-30 |
simulaneous 'def';
|
file | diff | annotate |
2005-11-27 |
wenzelm |
2005-11-27 |
* Provers/induct: obtain pattern;
|
file | diff | annotate |
2005-11-25 |
wenzelm |
2005-11-25 |
tuned;
|
file | diff | annotate |
2005-11-23 |
wenzelm |
2005-11-23 |
tuned;
|
file | diff | annotate |
2005-11-23 |
wenzelm |
2005-11-23 |
Provers/induct: definitional insts and fixing;
|
file | diff | annotate |
2005-11-23 |
wenzelm |
2005-11-23 |
tuned;
|
file | diff | annotate |
2005-11-10 |
wenzelm |
2005-11-10 |
renamed Thm.cgoal_of to Thm.cprem_of;
|
file | diff | annotate |
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 |