| 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
|
| 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
|