| Fri, 21 Nov 2008 13:17:43 +0100 |
paulson |
Strange. The proof worked in the 2008 release. In order to make it work now, the last line of the proof must be moved up two places. In other words, the first proof step is now returning its subgoals in a different order from before.
|
changeset |
files
|
| Fri, 21 Nov 2008 07:34:36 +0100 |
haftmann |
Name.binding
|
changeset |
files
|
| Thu, 20 Nov 2008 22:39:12 +0100 |
nipkow |
added optimizer
|
changeset |
files
|
| Thu, 20 Nov 2008 19:43:34 +0100 |
wenzelm |
reactivated some dead theories (based on hints by Mark Hillebrand);
|
changeset |
files
|
| Thu, 20 Nov 2008 19:06:05 +0100 |
haftmann |
Locale.local_note_qualified
|
changeset |
files
|
| Thu, 20 Nov 2008 19:06:03 +0100 |
haftmann |
fact table now using name bindings
|
changeset |
files
|
| Thu, 20 Nov 2008 19:06:02 +0100 |
haftmann |
dropped legacy naming code
|
changeset |
files
|
| Thu, 20 Nov 2008 14:55:28 +0100 |
haftmann |
tuned name bindings
|
changeset |
files
|
| Thu, 20 Nov 2008 14:55:25 +0100 |
haftmann |
using name bindings
|
changeset |
files
|
| Thu, 20 Nov 2008 14:51:40 +0100 |
haftmann |
name spaces and name bindings
|
changeset |
files
|
| Thu, 20 Nov 2008 10:29:35 +0100 |
ballarin |
Deleted debug message (PolyML).
|
changeset |
files
|
| Thu, 20 Nov 2008 00:03:55 +0100 |
wenzelm |
removed traces of former 'includes' element;
|
changeset |
files
|
| Thu, 20 Nov 2008 00:03:53 +0100 |
wenzelm |
updated generated files;
|
changeset |
files
|
| Thu, 20 Nov 2008 00:03:47 +0100 |
wenzelm |
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
|
changeset |
files
|
| Wed, 19 Nov 2008 18:15:31 +0100 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Wed, 19 Nov 2008 17:55:18 +0100 |
nipkow |
fixed
|
changeset |
files
|
| Wed, 19 Nov 2008 17:54:55 +0100 |
nipkow |
Added new fold operator and renamed the old oe to fold_image.
|
changeset |
files
|
| Wed, 19 Nov 2008 17:04:29 +0100 |
ballarin |
Type inference for elements through syntax module.
|
changeset |
files
|
| Wed, 19 Nov 2008 17:03:13 +0100 |
ballarin |
Use 'if' in connection with 'is_some' and 'the'.
|
changeset |
files
|
| Wed, 19 Nov 2008 17:00:00 +0100 |
ballarin |
Basic types not qualified.
|
changeset |
files
|
| Wed, 19 Nov 2008 16:58:33 +0100 |
ballarin |
Enable switching to new locales during session.
|
changeset |
files
|
| Wed, 19 Nov 2008 08:58:57 +0100 |
haftmann |
explicit inhabitance proof
|
changeset |
files
|
| Tue, 18 Nov 2008 22:25:36 +0100 |
wenzelm |
fulfill_proof/thm_proof: commuted lazyness;
|
changeset |
files
|
| Tue, 18 Nov 2008 22:25:30 +0100 |
wenzelm |
fulfill_proof/thm_proof: commuted lazyness;
|
changeset |
files
|
| Tue, 18 Nov 2008 21:17:14 +0100 |
krauss |
removed lemmas called lemma1 and lemma2
|
changeset |
files
|
| Tue, 18 Nov 2008 18:25:59 +0100 |
wenzelm |
force_proofs after cumulative use_thys;
|
changeset |
files
|
| Tue, 18 Nov 2008 18:25:55 +0100 |
wenzelm |
signed_string_of_int for priorities;
|
changeset |
files
|
| Tue, 18 Nov 2008 18:25:52 +0100 |
wenzelm |
added force_proofs;
|
changeset |
files
|
| Tue, 18 Nov 2008 18:25:49 +0100 |
wenzelm |
added force_proofs (based on thms ever passed through enter_thms);
|
changeset |
files
|
| Tue, 18 Nov 2008 18:25:45 +0100 |
wenzelm |
tuned;
|
changeset |
files
|