| 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
|
| 2005-12-21 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2005-12-21 |
wenzelm |
* induct: improved treatment of mutual goals and mutual rules;
|
file |
diff |
annotate
|
| 2005-12-21 |
haftmann |
discontinued unflat in favour of burrow and burrow_split
|
file |
diff |
annotate
|
| 2005-12-20 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2005-12-16 |
haftmann |
re-arranged tuples (theory * 'a) to ('a * theory) in Pure
|
file |
diff |
annotate
|
| 2005-12-13 |
wenzelm |
Provers/induct: coinduct;
|
file |
diff |
annotate
|
| 2005-12-08 |
wenzelm |
removed hint for Classical.swap, which is not really user-level anyway;
|
file |
diff |
annotate
|
| 2005-12-08 |
wenzelm |
* HOL: Theorem 'swap' is no longer bound at the ML top-level.
|
file |
diff |
annotate
|
| 2005-11-30 |
wenzelm |
simulaneous 'def';
|
file |
diff |
annotate
|
| 2005-11-27 |
wenzelm |
* Provers/induct: obtain pattern;
|
file |
diff |
annotate
|
| 2005-11-25 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2005-11-23 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2005-11-23 |
wenzelm |
Provers/induct: definitional insts and fixing;
|
file |
diff |
annotate
|
| 2005-11-23 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2005-11-10 |
wenzelm |
renamed Thm.cgoal_of to Thm.cprem_of;
|
file |
diff |
annotate
|
| 2005-10-31 |
haftmann |
nth_*, fold_index refined
|
file |
diff |
annotate
|
| 2005-10-28 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2005-10-28 |
wenzelm |
* Pure/Isar: literal facts;
|
file |
diff |
annotate
|
| 2005-10-27 |
wenzelm |
* HOL: alternative iff syntax;
|
file |
diff |
annotate
|
| 2005-10-27 |
haftmann |
added module Pure/General/rat.ML
|
file |
diff |
annotate
|
| 2005-10-21 |
wenzelm |
* Legacy goal package: reduced interface to the bare minimum required to keep existing proof scripts running.
|
file |
diff |
annotate
|
| 2005-10-19 |
wenzelm |
* Theory syntax: discontinued non-Isar format and old Isar headers;
|
file |
diff |
annotate
|
| 2005-10-18 |
wenzelm |
Simplifier.context/theory_context;
|
file |
diff |
annotate
|
| 2005-10-17 |
wenzelm |
* Simplifier: simpset of a running simplification process contains a proof context;
|
file |
diff |
annotate
|
| 2005-10-17 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2005-10-14 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2005-10-14 |
wenzelm |
* antiquotations ML_type, ML_struct;
|
file |
diff |
annotate
|
| 2005-10-09 |
webertj |
Tactics sat and satx reimplemented, several improvements
|
file |
diff |
annotate
|
| 2005-10-08 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| 2005-10-07 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2005-10-07 |
wenzelm |
added dummy variable binding;
|
file |
diff |
annotate
|
| 2005-10-04 |
wenzelm |
* Command 'find_theorems': support * wildcard in name: criterion.
|
file |
diff |
annotate
|
| 2005-09-29 |
wenzelm |
pdfsetup.sty: better not rely on ifpdf.sty;
|
file |
diff |
annotate
|
| 2005-09-29 |
wenzelm |
Isabelle2005 (October 2005);
|
file |
diff |
annotate
|
| 2005-09-28 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2005-09-28 |
webertj |
pointer to HOL/ex/SAT_Examples.thy added
|
file |
diff |
annotate
|
| 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
|