| Mon, 29 Sep 2008 12:31:59 +0200 |
haftmann |
clarified dependencies between arith tools
|
changeset |
files
|
| Mon, 29 Sep 2008 12:31:58 +0200 |
haftmann |
separate HOL-Main image
|
changeset |
files
|
| Mon, 29 Sep 2008 12:31:57 +0200 |
haftmann |
polished code generator setup
|
changeset |
files
|
| Mon, 29 Sep 2008 12:31:56 +0200 |
haftmann |
added theory antiquotation
|
changeset |
files
|
| Mon, 29 Sep 2008 11:46:52 +0200 |
wenzelm |
tuned comments;
|
changeset |
files
|
| Mon, 29 Sep 2008 11:46:47 +0200 |
wenzelm |
handle _ should be avoided (spurious Interrupt will spoil the game);
|
changeset |
files
|
| Mon, 29 Sep 2008 10:58:04 +0200 |
wenzelm |
added norm_export_morphism;
|
changeset |
files
|
| Mon, 29 Sep 2008 10:58:03 +0200 |
wenzelm |
added exit_global, exit_result, exit_result_global;
|
changeset |
files
|
| Mon, 29 Sep 2008 10:58:01 +0200 |
wenzelm |
LocalTheory.exit_global;
|
changeset |
files
|
| Sun, 28 Sep 2008 14:46:51 +0200 |
wenzelm |
HOL no longer depends on HOL-Plain;
|
changeset |
files
|
| Sun, 28 Sep 2008 14:40:43 +0200 |
wenzelm |
setmp_noncritical;
|
changeset |
files
|
| Sun, 28 Sep 2008 12:42:35 +0200 |
wenzelm |
join earlier promises first;
|
changeset |
files
|
| Sun, 28 Sep 2008 12:23:45 +0200 |
wenzelm |
proper setmp_thread_data for nested execute (cf. join_loop);
|
changeset |
files
|
| Sun, 28 Sep 2008 12:23:44 +0200 |
wenzelm |
promise_result: enforce strictly sequential dependencies, via serial numbers;
|
changeset |
files
|
| Sun, 28 Sep 2008 09:25:24 +0200 |
kleing |
do not cvs update for doc test (switching to mercurial, update done outside
|
changeset |
files
|
| Sun, 28 Sep 2008 09:13:46 +0200 |
kleing |
use mercurial repository for isatest
|
changeset |
files
|
| Sun, 28 Sep 2008 00:00:55 +0200 |
wenzelm |
thread_data: include thread name, export access;
|
changeset |
files
|
| Sat, 27 Sep 2008 19:35:00 +0200 |
wenzelm |
setmp_noncritical;
|
changeset |
files
|
| Sat, 27 Sep 2008 18:18:08 +0200 |
wenzelm |
dequeue_towards: return bound for unfinished tasks;
|
changeset |
files
|
| Sat, 27 Sep 2008 18:18:07 +0200 |
wenzelm |
moved release_results to future.ML;
|
changeset |
files
|
| Sat, 27 Sep 2008 18:18:06 +0200 |
wenzelm |
added release_results (formerly in par_list.ML);
|
changeset |
files
|
| Sat, 27 Sep 2008 18:18:05 +0200 |
wenzelm |
Future.release_results;
|
changeset |
files
|
| Sat, 27 Sep 2008 15:37:01 +0200 |
wenzelm |
more tracing;
|
changeset |
files
|
| Sat, 27 Sep 2008 15:20:39 +0200 |
wenzelm |
Theory.checkpoint for main operations, admits concurrent proofs;
|
changeset |
files
|
| Sat, 27 Sep 2008 15:20:37 +0200 |
wenzelm |
promise: include check into future body, i.e. joined results are always valid;
|
changeset |
files
|
| Sat, 27 Sep 2008 15:20:36 +0200 |
wenzelm |
proper transfer of theorems that involve classes being instantiated here;
|
changeset |
files
|
| Sat, 27 Sep 2008 14:26:06 +0200 |
wenzelm |
HOL_USEDIR_OPTIONS no longer applies to HOL-Plain (main HOL is rebuilt from Pure);
|
changeset |
files
|
| Fri, 26 Sep 2008 19:07:56 +0200 |
wenzelm |
eliminated polymorphic equality;
|
changeset |
files
|
| Fri, 26 Sep 2008 17:24:15 +0200 |
wenzelm |
added subset operation;
|
changeset |
files
|
| Fri, 26 Sep 2008 14:53:10 +0200 |
berghofe |
Added fresh_star_const.
|
changeset |
files
|
| Fri, 26 Sep 2008 14:52:27 +0200 |
berghofe |
Added some more theorems to NominalData.
|
changeset |
files
|
| Fri, 26 Sep 2008 14:51:27 +0200 |
berghofe |
Added some more lemmas that are useful in proof of strong induction rule.
|
changeset |
files
|
| Fri, 26 Sep 2008 09:10:02 +0200 |
haftmann |
removed obsolete name convention "func"
|
changeset |
files
|
| Fri, 26 Sep 2008 09:09:53 +0200 |
haftmann |
fixed typo
|
changeset |
files
|
| Fri, 26 Sep 2008 09:09:52 +0200 |
haftmann |
clarified function transformator interface
|
changeset |
files
|
| Fri, 26 Sep 2008 09:09:51 +0200 |
haftmann |
op = vs. eq
|
changeset |
files
|
| Thu, 25 Sep 2008 20:34:21 +0200 |
wenzelm |
moved future_scheduler flag to skip_proof.ML;
|
changeset |
files
|
| Thu, 25 Sep 2008 20:34:20 +0200 |
wenzelm |
added future_scheduler (from thy_info.ML);
|
changeset |
files
|
| Thu, 25 Sep 2008 20:34:19 +0200 |
wenzelm |
simplified promise;
|
changeset |
files
|
| Thu, 25 Sep 2008 20:34:18 +0200 |
wenzelm |
simplified Thm.promise;
|
changeset |
files
|
| Thu, 25 Sep 2008 20:34:17 +0200 |
wenzelm |
explicit checkpoint for low-level (global) theory operations admits concurrent SkipProof.prove;
|
changeset |
files
|
| Thu, 25 Sep 2008 20:34:15 +0200 |
wenzelm |
explicit checkpoint for low-level (global) theory operations, admits concurrent proofs;
|
changeset |
files
|
| Thu, 25 Sep 2008 19:15:50 +0200 |
haftmann |
circumvent problem with code redundancy
|
changeset |
files
|
| Thu, 25 Sep 2008 16:05:52 +0200 |
haftmann |
clarifed redundancy policy
|
changeset |
files
|
| Thu, 25 Sep 2008 14:37:32 +0200 |
wenzelm |
tuned comments;
|
changeset |
files
|
| Thu, 25 Sep 2008 14:35:03 +0200 |
wenzelm |
added release_results;
|
changeset |
files
|
| Thu, 25 Sep 2008 14:35:02 +0200 |
wenzelm |
abtract types: plain datatype with opaque signature matching;
|
changeset |
files
|
| Thu, 25 Sep 2008 14:35:01 +0200 |
wenzelm |
prove: error with original thread position;
|
changeset |
files
|
| Thu, 25 Sep 2008 13:21:13 +0200 |
wenzelm |
explicit type OrdList.T;
|
changeset |
files
|
| Thu, 25 Sep 2008 11:14:01 +0200 |
haftmann |
(temporary workaround)
|
changeset |
files
|
| Thu, 25 Sep 2008 10:17:23 +0200 |
haftmann |
(temporal deactivation)
|
changeset |
files
|
| Thu, 25 Sep 2008 10:17:22 +0200 |
haftmann |
non left-linear equations for nbe
|
changeset |
files
|
| Thu, 25 Sep 2008 09:28:08 +0200 |
haftmann |
non left-linear equations for nbe
|
changeset |
files
|
| Thu, 25 Sep 2008 09:28:07 +0200 |
haftmann |
map_force
|
changeset |
files
|
| Thu, 25 Sep 2008 09:28:06 +0200 |
haftmann |
matchess
|
changeset |
files
|
| Thu, 25 Sep 2008 09:28:05 +0200 |
haftmann |
burrow_fst
|
changeset |
files
|
| Thu, 25 Sep 2008 09:28:03 +0200 |
haftmann |
discontinued special treatment of op = vs. eq_class.eq
|
changeset |
files
|
| Wed, 24 Sep 2008 19:39:25 +0200 |
wenzelm |
report: produce individual status messages;
|
changeset |
files
|
| Wed, 24 Sep 2008 19:33:14 +0200 |
wenzelm |
protocol change: remapped message codes to make room for nested system messages (e.g. for protocol proxy);
|
changeset |
files
|
| Wed, 24 Sep 2008 19:33:13 +0200 |
wenzelm |
protocol change: remapped message codes to make room for nested system messages (e.g. for protocol proxy);
|
changeset |
files
|