| Fri, 23 Dec 2005 14:33:28 +0100 |
haftmann |
is_prefix
|
file |
diff |
annotate
|
| Thu, 22 Dec 2005 00:41:26 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 22 Dec 2005 00:29:12 +0100 |
wenzelm |
* induct: improved treatment of mutual goals and mutual rules;
|
file |
diff |
annotate
|
| Wed, 21 Dec 2005 13:25:20 +0100 |
haftmann |
discontinued unflat in favour of burrow and burrow_split
|
file |
diff |
annotate
|
| Tue, 20 Dec 2005 22:06:00 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 16 Dec 2005 16:00:58 +0100 |
haftmann |
re-arranged tuples (theory * 'a) to ('a * theory) in Pure
|
file |
diff |
annotate
|
| Tue, 13 Dec 2005 19:32:06 +0100 |
wenzelm |
Provers/induct: coinduct;
|
file |
diff |
annotate
|
| Thu, 08 Dec 2005 20:15:34 +0100 |
wenzelm |
removed hint for Classical.swap, which is not really user-level anyway;
|
file |
diff |
annotate
|
| Thu, 08 Dec 2005 12:50:02 +0100 |
wenzelm |
* HOL: Theorem 'swap' is no longer bound at the ML top-level.
|
file |
diff |
annotate
|
| Wed, 30 Nov 2005 22:52:46 +0100 |
wenzelm |
simulaneous 'def';
|
file |
diff |
annotate
|
| Sun, 27 Nov 2005 20:06:24 +0100 |
wenzelm |
* Provers/induct: obtain pattern;
|
file |
diff |
annotate
|
| Fri, 25 Nov 2005 18:58:34 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 23 Nov 2005 20:29:36 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 23 Nov 2005 18:52:05 +0100 |
wenzelm |
Provers/induct: definitional insts and fixing;
|
file |
diff |
annotate
|
| Wed, 23 Nov 2005 18:52:00 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 10 Nov 2005 20:57:11 +0100 |
wenzelm |
renamed Thm.cgoal_of to Thm.cprem_of;
|
file |
diff |
annotate
|
| Mon, 31 Oct 2005 16:35:15 +0100 |
haftmann |
nth_*, fold_index refined
|
file |
diff |
annotate
|
| Fri, 28 Oct 2005 22:37:57 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 28 Oct 2005 22:27:41 +0200 |
wenzelm |
* Pure/Isar: literal facts;
|
file |
diff |
annotate
|
| Thu, 27 Oct 2005 13:59:06 +0200 |
wenzelm |
* HOL: alternative iff syntax;
|
file |
diff |
annotate
|
| Thu, 27 Oct 2005 08:14:05 +0200 |
haftmann |
added module Pure/General/rat.ML
|
file |
diff |
annotate
|
| Fri, 21 Oct 2005 18:16:57 +0200 |
wenzelm |
* Legacy goal package: reduced interface to the bare minimum required to keep existing proof scripts running.
|
file |
diff |
annotate
|
| Wed, 19 Oct 2005 21:52:30 +0200 |
wenzelm |
* Theory syntax: discontinued non-Isar format and old Isar headers;
|
file |
diff |
annotate
|
| Tue, 18 Oct 2005 17:59:23 +0200 |
wenzelm |
Simplifier.context/theory_context;
|
file |
diff |
annotate
|
| Mon, 17 Oct 2005 23:10:25 +0200 |
wenzelm |
* Simplifier: simpset of a running simplification process contains a proof context;
|
file |
diff |
annotate
|
| Mon, 17 Oct 2005 23:10:16 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 15 Oct 2005 00:14:30 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 15 Oct 2005 00:08:14 +0200 |
wenzelm |
* antiquotations ML_type, ML_struct;
|
file |
diff |
annotate
|
| Sun, 09 Oct 2005 17:06:03 +0200 |
webertj |
Tactics sat and satx reimplemented, several improvements
|
file |
diff |
annotate
|
| Sat, 08 Oct 2005 23:36:01 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|