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