| Sun, 23 Nov 2008 17:27:15 +0100 |
wenzelm |
eliminated finish_proof, keep pre/post normalization of results separate;
|
changeset |
files
|
| Sun, 23 Nov 2008 17:25:56 +0100 |
wenzelm |
future: norm_proof after make_result reduces memory requirements but increases runtime (factor 1.5 for both for HOL with proof terms);
|
changeset |
files
|
| Fri, 21 Nov 2008 18:02:19 +0100 |
ballarin |
Regression tests for new locale implementation.
|
changeset |
files
|
| Fri, 21 Nov 2008 18:01:39 +0100 |
ballarin |
add_locale functional.
|
changeset |
files
|
| Fri, 21 Nov 2008 15:54:53 +0100 |
paulson |
Added a line that was missing from the definition
|
changeset |
files
|
| Fri, 21 Nov 2008 14:21:42 +0100 |
krauss |
added binary logarithm
|
changeset |
files
|
| 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
|
| Tue, 18 Nov 2008 18:25:42 +0100 |
wenzelm |
eliminated rewrite_tac/fold_tac, which are not well-formed tactics due to change of main conclusion;
|
changeset |
files
|
| Tue, 18 Nov 2008 18:25:10 +0100 |
wenzelm |
moved table of standard Isabelle symbols to isar-ref manual;
|
changeset |
files
|
| Tue, 18 Nov 2008 18:22:49 +0100 |
wenzelm |
added isabelle-implementation manual;
|
changeset |
files
|
| Tue, 18 Nov 2008 13:19:13 +0100 |
wenzelm |
disabled threads -- as advertized;
|
changeset |
files
|
| Tue, 18 Nov 2008 11:26:59 +0100 |
wenzelm |
changes by Fabian Immler:
|
changeset |
files
|
| Tue, 18 Nov 2008 09:41:23 +0100 |
ballarin |
Code for switching to new locales.
|
changeset |
files
|
| Tue, 18 Nov 2008 09:40:44 +0100 |
ballarin |
add_thmss
|
changeset |
files
|
| Tue, 18 Nov 2008 09:40:06 +0100 |
ballarin |
Activate elements moved to element.ML.
|
changeset |
files
|
| Tue, 18 Nov 2008 00:11:06 +0100 |
wenzelm |
finish: force proofs;
|
changeset |
files
|
| Mon, 17 Nov 2008 23:34:35 +0100 |
wenzelm |
finish_proof: undefined promises may occur here;
|
changeset |
files
|
| Mon, 17 Nov 2008 23:17:13 +0100 |
wenzelm |
tuned promise/fullfill;
|
changeset |
files
|
| Mon, 17 Nov 2008 23:17:11 +0100 |
wenzelm |
unified treatment of PAxm/Oracle/Promise in basic proof term operations;
|
changeset |
files
|
| Mon, 17 Nov 2008 21:36:48 +0100 |
wenzelm |
removed Induct/Mutil.thy -- the file has been moved to AFP;
|
changeset |
files
|
| Mon, 17 Nov 2008 21:28:46 +0100 |
wenzelm |
simplified thm_deps -- no need to build a graph datastructure;
|
changeset |
files
|
| Mon, 17 Nov 2008 21:13:48 +0100 |
wenzelm |
removed Induct/Mutil.thy -- the file has been moved to AFP;
|
changeset |
files
|
| Mon, 17 Nov 2008 17:25:02 +0100 |
nipkow |
-> AFP
|
changeset |
files
|
| Mon, 17 Nov 2008 17:00:55 +0100 |
haftmann |
tuned unfold_locales invocation
|
changeset |
files
|
| Mon, 17 Nov 2008 17:00:27 +0100 |
haftmann |
explicit name morphism function for locale interpretation
|
changeset |
files
|
| Mon, 17 Nov 2008 17:00:26 +0100 |
haftmann |
Name.name_with_prefix (temporarily)
|
changeset |
files
|
| Mon, 17 Nov 2008 17:00:22 +0100 |
haftmann |
adjusted locale signature to *_cmd convention
|
changeset |
files
|
| Mon, 17 Nov 2008 17:00:21 +0100 |
haftmann |
whitespace tuning
|
changeset |
files
|
| Mon, 17 Nov 2008 14:03:39 +0100 |
ballarin |
Generic activation of locales.
|
changeset |
files
|
| Sun, 16 Nov 2008 22:12:44 +0100 |
wenzelm |
proof_body/pthm: removed redundant types field;
|
changeset |
files
|
| Sun, 16 Nov 2008 22:12:43 +0100 |
wenzelm |
put_name/thm_proof: promises are filled with fulfilled proofs;
|
changeset |
files
|