| Sat, 01 Aug 2009 20:34:34 +0200 |
wenzelm |
updated Variable.import;
|
changeset |
files
|
| Sat, 01 Aug 2009 00:39:51 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Sat, 01 Aug 2009 00:39:45 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 31 Jul 2009 11:34:14 +0200 |
wenzelm |
modernized generated example session;
|
changeset |
files
|
| Fri, 31 Jul 2009 23:31:11 +0200 |
boehmes |
added Mirabelle
|
changeset |
files
|
| Fri, 31 Jul 2009 23:30:21 +0200 |
boehmes |
Quickcheck callable from ML
|
changeset |
files
|
| Sat, 01 Aug 2009 00:17:03 +0200 |
wenzelm |
future scheduler: uninterruptible cancelation;
|
changeset |
files
|
| Sat, 01 Aug 2009 00:09:45 +0200 |
wenzelm |
renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
|
changeset |
files
|
| Thu, 30 Jul 2009 23:50:11 +0200 |
wenzelm |
recovered polyml-5.2 -- need to reload ML-Systems/multithreading.ML after overriding Thread structures;
|
changeset |
files
|
| Thu, 30 Jul 2009 23:37:53 +0200 |
wenzelm |
tuned tracing;
|
changeset |
files
|
| Thu, 30 Jul 2009 23:23:52 +0200 |
wenzelm |
ISABELLE_USEDIR_OPTIONS: -q 2 by default;
|
changeset |
files
|
| Thu, 30 Jul 2009 23:09:29 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 30 Jul 2009 21:27:15 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 30 Jul 2009 08:18:22 +0200 |
haftmann |
merged
|
changeset |
files
|
| Wed, 29 Jul 2009 16:54:20 +0200 |
haftmann |
cleaned up abstract tuple operations and named them consistently
|
changeset |
files
|
| Wed, 29 Jul 2009 16:48:34 +0200 |
haftmann |
cleaned up abstract tuple operations and named them consistently
|
changeset |
files
|
| Thu, 30 Jul 2009 23:06:06 +0200 |
wenzelm |
added Multithreading.sync_wait, which turns enabled interrupts to sync ones, to ensure that wait will reaquire its lock when interrupted;
|
changeset |
files
|
| Thu, 30 Jul 2009 18:43:52 +0200 |
wenzelm |
trancl_tac etc.: back to static context -- problem was caused by bad solver in AFP/JiveDataStoreModel;
|
changeset |
files
|
| Thu, 30 Jul 2009 17:54:57 +0200 |
wenzelm |
retrofit: more precise handling of locally introduced schematic variables (avoid zero_var_indexes);
|
changeset |
files
|
| Thu, 30 Jul 2009 12:20:43 +0200 |
wenzelm |
qualified Subgoal.FOCUS;
|
changeset |
files
|
| Thu, 30 Jul 2009 11:23:57 +0200 |
wenzelm |
FOCUS_PREMS as full replacement for METAHYPS, where the conclusion may still contain schematic variables;
|
changeset |
files
|
| Thu, 30 Jul 2009 11:23:17 +0200 |
wenzelm |
focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
|
changeset |
files
|
| Thu, 30 Jul 2009 01:14:40 +0200 |
wenzelm |
Variable.importT/import: return full instantiations, tuned;
|
changeset |
files
|
| Thu, 30 Jul 2009 01:12:33 +0200 |
wenzelm |
added certify_inst, certify_instantiate;
|
changeset |
files
|
| Wed, 29 Jul 2009 22:38:35 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 29 Jul 2009 22:34:31 +0200 |
wenzelm |
trans_tac: use theory from goal state, not the static context, which seems to be outdated under certain circumstances (why?);
|
changeset |
files
|
| Wed, 29 Jul 2009 21:40:04 +0200 |
wenzelm |
proper Jinja-Slicing;
|
changeset |
files
|
| Wed, 29 Jul 2009 19:36:22 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 29 Jul 2009 16:43:02 +0200 |
haftmann |
merged
|
changeset |
files
|
| Wed, 29 Jul 2009 16:42:47 +0200 |
haftmann |
abstractions: desymbolize name hint
|
changeset |
files
|
| Wed, 29 Jul 2009 16:42:47 +0200 |
haftmann |
added numeral code postprocessor rules on type int
|
changeset |
files
|
| Wed, 29 Jul 2009 12:13:21 +0200 |
nipkow |
sos comments modified
|
changeset |
files
|
| Wed, 29 Jul 2009 12:12:01 +0200 |
nipkow |
sos documentation
|
changeset |
files
|
| Wed, 29 Jul 2009 09:06:49 +0200 |
nipkow |
Added remote-SOS changes by Philipp Meyer
|
changeset |
files
|
| Fri, 24 Jul 2009 13:56:02 +0200 |
Philipp Meyer |
Functionality for sum of squares to call a remote csdp prover
|
changeset |
files
|
| Tue, 28 Jul 2009 20:26:39 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 28 Jul 2009 13:38:13 +0200 |
haftmann |
updated generated document
|
changeset |
files
|
| Tue, 28 Jul 2009 13:37:40 +0200 |
haftmann |
reinserted legacy ML function
|
changeset |
files
|
| Tue, 28 Jul 2009 13:37:09 +0200 |
haftmann |
Set.UNIV and Set.empty are mere abbreviations for top and bot
|
changeset |
files
|
| Tue, 28 Jul 2009 13:37:08 +0200 |
haftmann |
explicit is better than implicit
|
changeset |
files
|
| Wed, 29 Jul 2009 19:35:10 +0200 |
wenzelm |
Meson.first_order_resolve: avoid handle _;
|
changeset |
files
|
| Wed, 29 Jul 2009 00:09:14 +0200 |
wenzelm |
removed old global get_claset/map_claset;
|
changeset |
files
|
| Tue, 28 Jul 2009 20:03:58 +0200 |
wenzelm |
eliminated METAHYPS;
|
changeset |
files
|
| Tue, 28 Jul 2009 19:49:42 +0200 |
wenzelm |
Future.shutdown before loading sequentially -- workaround scheduler deadlock;
|
changeset |
files
|
| Tue, 28 Jul 2009 18:17:36 +0200 |
wenzelm |
ResAxioms.neg_conjecture_clauses: proper context;
|
changeset |
files
|
| Tue, 28 Jul 2009 18:17:35 +0200 |
wenzelm |
neg_conjecture_clauses, neg_clausify_tac: proper context, eliminated METAHYPS;
|
changeset |
files
|
| Tue, 28 Jul 2009 18:17:35 +0200 |
wenzelm |
Hilbert_Classical: sequential loading due to @{prf}, which joins within a critical section (via options);
|
changeset |
files
|
| Tue, 28 Jul 2009 16:30:23 +0200 |
wenzelm |
eliminated separate Future.enabled -- let Future.join fail explicitly in critical section, instead of entering sequential mode silently;
|
changeset |
files
|
| Tue, 28 Jul 2009 16:28:49 +0200 |
wenzelm |
non-critical use_thy;
|
changeset |
files
|
| Tue, 28 Jul 2009 15:10:15 +0200 |
wenzelm |
future result: Synchronized.var;
|
changeset |
files
|
| Tue, 28 Jul 2009 15:05:18 +0200 |
wenzelm |
added unsynchronized Synchronized.peek;
|
changeset |
files
|
| Tue, 28 Jul 2009 14:54:53 +0200 |
wenzelm |
group status: Synchronized.var;
|
changeset |
files
|
| Tue, 28 Jul 2009 14:43:46 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 28 Jul 2009 14:35:27 +0200 |
wenzelm |
Task_Queue.dequeue: explicit thread;
|
changeset |
files
|
| Tue, 28 Jul 2009 14:29:25 +0200 |
wenzelm |
more precise treatment of scheduler_event: continous pulse (50ms) instead of flooding, which was burning many CPU cycles in spare threads;
|
changeset |
files
|
| Tue, 28 Jul 2009 14:11:15 +0200 |
wenzelm |
interruptible_task: unified treatment of Multithreading.with_attributes (cf. 9f6461b1c9cc);
|
changeset |
files
|
| Tue, 28 Jul 2009 14:04:33 +0200 |
wenzelm |
misc tuning;
|
changeset |
files
|
| Tue, 28 Jul 2009 08:49:03 +0200 |
krauss |
tuned
|
changeset |
files
|
| Tue, 28 Jul 2009 08:48:56 +0200 |
krauss |
moved obsolete same_fst to Recdef.thy
|
changeset |
files
|
| Tue, 28 Jul 2009 08:48:48 +0200 |
krauss |
adapted doc to type of "op O"
|
changeset |
files
|