| Sat, 21 Jan 2006 23:07:26 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 21 Jan 2006 23:02:30 +0100 |
wenzelm |
* ML: simplified type attribute;
|
file |
diff |
annotate
|
| Thu, 19 Jan 2006 21:22:27 +0100 |
wenzelm |
* ML/Isar: theory setup has type (theory -> theory);
|
file |
diff |
annotate
|
| Sun, 15 Jan 2006 20:04:05 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 15 Jan 2006 20:00:59 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 15 Jan 2006 19:58:57 +0100 |
wenzelm |
* Classical: optional weight for attributes;
|
file |
diff |
annotate
|
| Sat, 14 Jan 2006 17:20:51 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 14 Jan 2006 17:15:24 +0100 |
wenzelm |
* ML/Isar: simplified treatment of user-level errors;
|
file |
diff |
annotate
|
| Fri, 13 Jan 2006 14:43:09 +0100 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Tue, 10 Jan 2006 19:36:59 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 10 Jan 2006 19:33:42 +0100 |
wenzelm |
* ML: generic context, data, attributes;
|
file |
diff |
annotate
|
| Sat, 07 Jan 2006 12:26:23 +0100 |
wenzelm |
* Provers/induct: improved simultaneous goals -- nested cases;
|
file |
diff |
annotate
|
| Fri, 06 Jan 2006 15:18:19 +0100 |
wenzelm |
Pure/Isar: Toplevel.theory_to_proof admits transactions that modify the theory;
|
file |
diff |
annotate
|
| Wed, 04 Jan 2006 01:04:59 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 04 Jan 2006 01:00:52 +0100 |
wenzelm |
* Pure/Isar: Toplevel.theory_theory_to_proof;
|
file |
diff |
annotate
|
| Tue, 03 Jan 2006 15:44:39 +0100 |
paulson |
Provers/classical: stricter checks to ensure that supplied intro, dest and
|
file |
diff |
annotate
|
| Tue, 03 Jan 2006 11:31:15 +0100 |
haftmann |
rearranged burrow_split to fold_burrow to allow composition with fold_map
|
file |
diff |
annotate
|
| Tue, 03 Jan 2006 00:06:18 +0100 |
wenzelm |
* Pure/Isar: new command 'unfolding';
|
file |
diff |
annotate
|
| Sat, 31 Dec 2005 21:49:44 +0100 |
wenzelm |
* Provers/classical: removed obsolete classical version of elim_format;
|
file |
diff |
annotate
|
| Fri, 23 Dec 2005 15:21:05 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 23 Dec 2005 15:18:13 +0100 |
wenzelm |
* Provers/induct: support simultaneous goals with mutual rules;
|
file |
diff |
annotate
|
| 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
|