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