| Mon, 07 Jul 2014 16:06:46 +0200 |
desharna |
add helper function map_prod
|
changeset |
files
|
| Mon, 07 Jul 2014 16:06:46 +0200 |
desharna |
document property 'rel_cases'
|
changeset |
files
|
| Mon, 07 Jul 2014 16:06:46 +0200 |
desharna |
generate 'rel_cases' theorem for (co)datatypes
|
changeset |
files
|
| Sat, 05 Jul 2014 20:51:24 +0200 |
wenzelm |
update for release;
|
changeset |
files
|
| Sat, 05 Jul 2014 16:29:19 +0200 |
wenzelm |
Added tag Isabelle2014-RC0 for changeset 251ef0202e71
|
changeset |
files
|
| Sat, 05 Jul 2014 16:28:07 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Sat, 05 Jul 2014 13:39:53 +0200 |
wenzelm |
modernized definitions;
|
changeset |
files
|
| Sat, 05 Jul 2014 13:21:53 +0200 |
wenzelm |
proper plain_args to ensure that multi-argument overloading cannot escape pattern restriction (despite more liberal structural containment before 3ae3cc4b1eac);
|
changeset |
files
|
| Sat, 05 Jul 2014 16:07:23 +0200 |
haftmann |
CONTRIBUTORS
|
changeset |
files
|
| Sat, 05 Jul 2014 16:04:23 +0200 |
haftmann |
refrain from auxiliary abbreviation: be more explicit to the reader in situations where syntax translation does not apply;
|
changeset |
files
|
| Sat, 05 Jul 2014 12:04:25 +0200 |
wenzelm |
misc tuning for release;
|
changeset |
files
|
| Sat, 05 Jul 2014 11:19:37 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 05 Jul 2014 11:06:14 +0200 |
haftmann |
NEWS
|
changeset |
files
|
| Sat, 05 Jul 2014 11:01:53 +0200 |
haftmann |
prefer ac_simps collections over separate name bindings for add and mult
|
changeset |
files
|
| Sat, 05 Jul 2014 10:09:01 +0200 |
kleing |
added Tom's hyp_subst update
|
changeset |
files
|
| Fri, 04 Jul 2014 20:18:47 +0200 |
haftmann |
reduced name variants for assoc and commute on plus and mult
|
changeset |
files
|
| Fri, 04 Jul 2014 20:07:08 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 04 Jul 2014 17:41:35 +0200 |
wenzelm |
insist in explicit overloading;
|
changeset |
files
|
| Fri, 04 Jul 2014 17:19:03 +0200 |
wenzelm |
more uniform names;
|
changeset |
files
|
| Fri, 04 Jul 2014 16:50:57 +0200 |
wenzelm |
misc tuning for release;
|
changeset |
files
|
| Fri, 04 Jul 2014 15:50:28 +0200 |
wenzelm |
revived unchecked theory (see cebaf814ca6e);
|
changeset |
files
|
| Fri, 04 Jul 2014 15:46:13 +0200 |
wenzelm |
suppress completion of obscure keyword;
|
changeset |
files
|
| Fri, 04 Jul 2014 14:58:52 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 04 Jul 2014 14:52:05 +0200 |
wenzelm |
misc tuning for release;
|
changeset |
files
|
| Fri, 04 Jul 2014 11:39:34 +0200 |
wenzelm |
NEWS;
|
changeset |
files
|
| Thu, 03 Jul 2014 16:42:15 +0200 |
nipkow |
Tail recursion no longer supported by "function".
|
changeset |
files
|
| Thu, 03 Jul 2014 14:40:36 +0200 |
haftmann |
merged
|
changeset |
files
|
| Thu, 03 Jul 2014 09:55:16 +0200 |
Christian Sternagel |
weaker assumption for "list_emb_trans"; added lemma
|
changeset |
files
|
| Thu, 03 Jul 2014 09:55:15 +0200 |
Christian Sternagel |
added monotonicity lemma for list embedding
|
changeset |
files
|
| Thu, 03 Jul 2014 09:55:15 +0200 |
Christian Sternagel |
no built-in reflexivity of list embedding (which is more standard; now embedding is reflexive whenever the base-order is)
|
changeset |
files
|
| Thu, 03 Jul 2014 09:55:15 +0200 |
Christian Sternagel |
renamed "list_hembeq" into slightly shorter "list_emb"
|
changeset |
files
|
| Thu, 03 Jul 2014 12:17:55 +0200 |
wenzelm |
misc tuning;
|
changeset |
files
|
| Thu, 03 Jul 2014 11:31:25 +0200 |
desharna |
merge
|
changeset |
files
|
| Thu, 03 Jul 2014 11:30:23 +0200 |
desharna |
document property 'rel_intros'
|
changeset |
files
|
| Thu, 03 Jul 2014 11:30:02 +0200 |
desharna |
generate 'rel_intros' theorem for (co)datatypes
|
changeset |
files
|
| Wed, 11 Jun 2014 14:24:23 +1000 |
Thomas Sewell |
Hypsubst preserves equality hypotheses
|
changeset |
files
|
| Wed, 02 Jul 2014 17:34:45 +0200 |
wenzelm |
tuned grammar and spelling (cf. 0cf15843b82f);
|
changeset |
files
|
| Wed, 02 Jul 2014 17:01:51 +0200 |
desharna |
document property 'corec_code'
|
changeset |
files
|
| Wed, 02 Jul 2014 17:01:49 +0200 |
desharna |
generate 'corec_code' theorem for codatatypes
|
changeset |
files
|
| Wed, 02 Jul 2014 13:23:11 +0200 |
wenzelm |
modernized definitions;
|
changeset |
files
|
| Wed, 02 Jul 2014 13:06:07 +0200 |
wenzelm |
misc tuning and clarification;
|
changeset |
files
|
| Wed, 02 Jul 2014 12:12:26 +0200 |
wenzelm |
check 'case' variable bindings as for 'fix', which means internal names are rejected as usual;
|
changeset |
files
|
| Wed, 02 Jul 2014 08:03:50 +0200 |
haftmann |
optional exit hook for theory-like targets
|
changeset |
files
|
| Wed, 02 Jul 2014 08:03:49 +0200 |
haftmann |
restore exactly named target, prevent non-named targets to participate in the ad-hoc switch game
|
changeset |
files
|
| Wed, 02 Jul 2014 08:03:48 +0200 |
haftmann |
centralized (ad-hoc) switching of targets in named_target.ML
|
changeset |
files
|
| Tue, 01 Jul 2014 21:57:08 -0700 |
huffman |
add lemmas: polynomial div/mod distribute over addition
|
changeset |
files
|
| Tue, 01 Jul 2014 23:02:25 +0200 |
blanchet |
reverted 9512b867259c -- appears to break 'metis'
|
changeset |
files
|
| Tue, 01 Jul 2014 21:07:02 +0200 |
wenzelm |
clarified "axiomatization" -- minor rewording of this delicate concept;
|
changeset |
files
|
| Tue, 01 Jul 2014 20:47:25 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 01 Jul 2014 20:43:51 +0200 |
wenzelm |
more on ML options;
|
changeset |
files
|
| Tue, 01 Jul 2014 17:59:56 +0200 |
wenzelm |
redundant error position, to ensure the message is attached somewhere, despite the distortion of positions due to glued tokens;
|
changeset |
files
|
| Tue, 01 Jul 2014 17:16:11 +0200 |
immler |
overdue NEWS concerning c4daa97ac57a
|
changeset |
files
|
| Tue, 01 Jul 2014 16:09:51 +0100 |
paulson |
Merge
|
changeset |
files
|
| Tue, 01 Jul 2014 16:08:31 +0100 |
paulson |
for new release
|
changeset |
files
|
| Tue, 01 Jul 2014 17:06:54 +0200 |
desharna |
merge
|
changeset |
files
|
| Tue, 01 Jul 2014 17:01:48 +0200 |
desharna |
document property 'rel_induct'
|
changeset |
files
|
| Tue, 01 Jul 2014 17:01:28 +0200 |
desharna |
generate 'rel_induct' theorem for datatypes
|
changeset |
files
|
| Tue, 01 Jul 2014 16:49:25 +0200 |
blanchet |
fixed soundness bug in monotonicity-based type encodings -- the helper facts must be considered too
|
changeset |
files
|
| Tue, 01 Jul 2014 16:47:10 +0200 |
blanchet |
added hidden check to Sledgehammer fact filters, to avoid picking up facts like 'Nat.nat_induct0'
|
changeset |
files
|
| Tue, 01 Jul 2014 16:47:10 +0200 |
blanchet |
whitespace tuning
|
changeset |
files
|
| Tue, 01 Jul 2014 16:47:10 +0200 |
blanchet |
robustness in the face of ill-typed "unchecked" terms (e.g. case expressions)
|
changeset |
files
|
| Tue, 01 Jul 2014 16:47:10 +0200 |
blanchet |
use context instead of theory
|
changeset |
files
|
| Tue, 01 Jul 2014 16:47:10 +0200 |
blanchet |
fine-tuned methods
|
changeset |
files
|
| Tue, 01 Jul 2014 16:47:10 +0200 |
blanchet |
tuned message
|
changeset |
files
|
| Tue, 01 Jul 2014 16:47:10 +0200 |
blanchet |
updated docs
|
changeset |
files
|
| Tue, 01 Jul 2014 16:47:10 +0200 |
blanchet |
changed default MaSh engine
|
changeset |
files
|
| Tue, 01 Jul 2014 16:47:10 +0200 |
blanchet |
removed needless code
|
changeset |
files
|
| Tue, 01 Jul 2014 16:47:10 +0200 |
blanchet |
speed up MaSh a bit
|
changeset |
files
|
| Tue, 01 Jul 2014 16:47:10 +0200 |
blanchet |
mix NB and kNN
|
changeset |
files
|
| Tue, 01 Jul 2014 16:47:10 +0200 |
blanchet |
tuned (reordered) code
|
changeset |
files
|
| Tue, 01 Jul 2014 16:47:10 +0200 |
blanchet |
clean up MaSh export a bit
|
changeset |
files
|
| Tue, 01 Jul 2014 16:47:10 +0200 |
blanchet |
clean up MaSh evaluation driver
|
changeset |
files
|
| Tue, 01 Jul 2014 16:26:14 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 01 Jul 2014 15:19:43 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 01 Jul 2014 15:19:05 +0200 |
wenzelm |
clarified quasi-generic PIDE;
|
changeset |
files
|
| Tue, 01 Jul 2014 14:52:08 +0200 |
wenzelm |
misc updates for release;
|
changeset |
files
|
| Tue, 01 Jul 2014 14:05:05 +0200 |
wenzelm |
more release notes;
|
changeset |
files
|
| Tue, 01 Jul 2014 15:57:07 +0200 |
hoelzl |
Library/Tree: bst is preferred to be a function
|
changeset |
files
|
| Tue, 01 Jul 2014 15:25:27 +0200 |
hoelzl |
Library/Tree: use datatype_new, bst is an inductive predicate
|
changeset |
files
|
| Mon, 30 Jun 2014 15:45:25 +0200 |
hoelzl |
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
|
changeset |
files
|
| Mon, 30 Jun 2014 15:45:21 +0200 |
hoelzl |
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
|
changeset |
files
|
| Mon, 30 Jun 2014 15:45:03 +0200 |
hoelzl |
some lemmas about the indicator function; removed lemma sums_def2
|
changeset |
files
|
| Tue, 01 Jul 2014 11:06:31 +0200 |
traytel |
generate type correct terms in uncheck phase
|
changeset |
files
|
| Mon, 30 Jun 2014 15:23:00 +0200 |
wenzelm |
updated to sumatra_pdf-2.5.2;
|
changeset |
files
|
| Mon, 30 Jun 2014 10:53:37 +0200 |
wenzelm |
ProofGeneral-4.2-2 is optional component (including the traditional helper scripts);
|
changeset |
files
|
| Mon, 30 Jun 2014 10:34:28 +0200 |
wenzelm |
removed obsolete Isar system commands -- raw ML console is normally used for system tinkering;
|
changeset |
files
|
| Mon, 30 Jun 2014 10:10:32 +0200 |
wenzelm |
tuned comments;
|
changeset |
files
|
| Mon, 30 Jun 2014 10:00:16 +0200 |
wenzelm |
updated README;
|
changeset |
files
|
| Mon, 30 Jun 2014 09:43:44 +0200 |
wenzelm |
"isabelle tty" is superseded by "isabelle console";
|
changeset |
files
|
| Mon, 30 Jun 2014 09:31:32 +0200 |
wenzelm |
tuned description: fit into 80 chars terminal;
|
changeset |
files
|
| Mon, 30 Jun 2014 08:00:36 +0200 |
haftmann |
qualified String.explode and String.implode
|
changeset |
files
|
| Sun, 29 Jun 2014 21:07:53 +0200 |
blanchet |
removed non-existing MaSh component from list
|
changeset |
files
|
| Sun, 29 Jun 2014 18:02:18 +0200 |
haftmann |
modernized diagnostic options
|
changeset |
files
|
| Sun, 29 Jun 2014 18:30:24 +0200 |
blanchet |
use SMT2
|
changeset |
files
|
| Sun, 29 Jun 2014 18:28:27 +0200 |
blanchet |
compile
|
changeset |
files
|
| Sun, 29 Jun 2014 18:28:27 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Sun, 29 Jun 2014 18:28:27 +0200 |
blanchet |
killed Python version of MaSh, now that the SML version works adequately
|
changeset |
files
|
| Sat, 28 Jun 2014 22:13:23 +0200 |
haftmann |
tracing facilities for the code generator preprocessor
|
changeset |
files
|
| Sat, 28 Jun 2014 22:13:21 +0200 |
haftmann |
tuned interface
|
changeset |
files
|
| Sat, 28 Jun 2014 22:13:20 +0200 |
haftmann |
corrected handled exception
|
changeset |
files
|
| Sat, 28 Jun 2014 21:09:17 +0200 |
haftmann |
proper trading of variables;
|
changeset |
files
|
| Sat, 28 Jun 2014 21:09:15 +0200 |
haftmann |
modernized
|
changeset |
files
|
| Sat, 28 Jun 2014 18:02:33 +0200 |
wenzelm |
jedit_completion_immediate is enabled by default: let all users participate in slightly more ambitious symbol insertion;
|
changeset |
files
|
| Sat, 28 Jun 2014 17:54:34 +0200 |
wenzelm |
removed slightly odd fall-back on complete-word (NB: connection to default menu action is unclear);
|
changeset |
files
|
| Sat, 28 Jun 2014 15:50:48 +0200 |
wenzelm |
updated NEWS -- removed material that is already in the manual;
|
changeset |
files
|
| Sat, 28 Jun 2014 15:35:30 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Sat, 28 Jun 2014 15:34:43 +0200 |
wenzelm |
misc tuning;
|
changeset |
files
|
| Sat, 28 Jun 2014 11:19:58 +0200 |
wenzelm |
misc tuning;
|
changeset |
files
|
| Sat, 28 Jun 2014 11:44:22 +0200 |
haftmann |
CONTRIBUTORS
|
changeset |
files
|
| Sat, 28 Jun 2014 09:16:42 +0200 |
haftmann |
fact consolidation
|
changeset |
files
|
| Fri, 27 Jun 2014 22:08:55 +0200 |
wenzelm |
more tight Mailbox: single list is sufficient for single receiver, reverse outside critical section;
|
changeset |
files
|
| Fri, 27 Jun 2014 19:38:32 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 27 Jun 2014 16:04:56 +0200 |
wenzelm |
command 'print_term_bindings' supersedes 'print_binds';
|
changeset |
files
|
| Fri, 27 Jun 2014 15:41:26 +0200 |
wenzelm |
Proof General legacy;
|
changeset |
files
|
| Fri, 27 Jun 2014 15:30:57 +0200 |
wenzelm |
removed obsolete "isabelle unsymbolize";
|
changeset |
files
|
| Fri, 27 Jun 2014 15:24:56 +0200 |
wenzelm |
minor renovation of slightly odd and old README;
|
changeset |
files
|
| Fri, 27 Jun 2014 11:30:42 +0200 |
wenzelm |
sane environment defaults for Mac OS X, based on former App1/script -- e.g. relevant for MacTeX PATH;
|
changeset |
files
|
| Fri, 27 Jun 2014 19:21:58 +0200 |
blanchet |
tweaking
|
changeset |
files
|
| Fri, 27 Jun 2014 19:17:16 +0200 |
blanchet |
correctly take weights into consideration
|
changeset |
files
|
| Fri, 27 Jun 2014 18:27:37 +0200 |
blanchet |
tuned whitespace and parentheses
|
changeset |
files
|
| Fri, 27 Jun 2014 17:18:30 +0200 |
blanchet |
use right theory name for theorems in evaluation driver
|
changeset |
files
|
| Fri, 27 Jun 2014 17:05:22 +0200 |
blanchet |
killed dead code
|
changeset |
files
|
| Fri, 27 Jun 2014 16:52:50 +0200 |
blanchet |
reintroduced 'extra features' + only print message in verbose mode
|
changeset |
files
|
| Fri, 27 Jun 2014 14:20:50 +0200 |
blanchet |
got rid of hard-coded weights, now that we have TFIDF
|
changeset |
files
|
| Fri, 27 Jun 2014 12:06:22 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Fri, 27 Jun 2014 11:56:28 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Fri, 27 Jun 2014 11:38:15 +0200 |
blanchet |
reintroduced 'extra features' but with lower weight than before (to account for tfidf)
|
changeset |
files
|
| Fri, 27 Jun 2014 10:49:52 +0200 |
blanchet |
resolution modulo double negation
|
changeset |
files
|
| Fri, 27 Jun 2014 10:11:44 +0200 |
blanchet |
compile
|
changeset |
files
|
| Fri, 27 Jun 2014 10:11:44 +0200 |
blanchet |
merged two small theory files
|
changeset |
files
|
| Fri, 27 Jun 2014 10:11:44 +0200 |
blanchet |
tuned variable names
|
changeset |
files
|
| Fri, 27 Jun 2014 10:11:44 +0200 |
blanchet |
whitespace tuning
|
changeset |
files
|
| Fri, 27 Jun 2014 10:11:44 +0200 |
blanchet |
repaired BNF 'size' generation tactic for datatypes mixng old- and new-style datatypes on the right-hand side
|
changeset |
files
|
| Fri, 27 Jun 2014 00:21:11 +0100 |
paulson |
tiny refinements
|
changeset |
files
|
| Thu, 26 Jun 2014 22:50:02 +0200 |
wenzelm |
suppress documentation "how_to_prove_it" for now, notably for release;
|
changeset |
files
|
| Thu, 26 Jun 2014 22:18:09 +0200 |
wenzelm |
updated to jdk-7u60 -- back to stable Java 7 for Isabelle2014 release;
|
changeset |
files
|
| Thu, 26 Jun 2014 22:01:40 +0200 |
wenzelm |
updated generated file;
|
changeset |
files
|
| Thu, 26 Jun 2014 21:25:41 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 26 Jun 2014 19:46:07 +0200 |
wenzelm |
updated cygwin on server;
|
changeset |
files
|
| Thu, 26 Jun 2014 20:49:34 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Thu, 26 Jun 2014 20:32:31 +0200 |
blanchet |
reintroduced MaSh hints, this time as persistent creatures
|
changeset |
files
|
| Thu, 26 Jun 2014 19:40:58 +0200 |
blanchet |
always expand all paths
|
changeset |
files
|
| Thu, 26 Jun 2014 19:10:34 +0200 |
blanchet |
tuned output
|
changeset |
files
|
| Thu, 26 Jun 2014 18:57:20 +0200 |
blanchet |
tuned output
|
changeset |
files
|
| Thu, 26 Jun 2014 16:41:43 +0200 |
blanchet |
right array indexing
|
changeset |
files
|
| Thu, 26 Jun 2014 16:41:30 +0200 |
blanchet |
incremental learning when learing several facts
|
changeset |
files
|
| Thu, 26 Jun 2014 16:41:30 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Thu, 26 Jun 2014 16:41:30 +0200 |
blanchet |
more incremental learning of single fact
|
changeset |
files
|
| Thu, 26 Jun 2014 16:41:30 +0200 |
blanchet |
avoid needless (trivial) reordering on load
|
changeset |
files
|
| Thu, 26 Jun 2014 16:41:30 +0200 |
blanchet |
recompute learning data at learning time, not query time
|
changeset |
files
|
| Thu, 26 Jun 2014 16:41:30 +0200 |
blanchet |
imported patch killed_num_known_facts0
|
changeset |
files
|
| Thu, 26 Jun 2014 13:36:25 +0200 |
blanchet |
refactoring
|
changeset |
files
|
| Thu, 26 Jun 2014 13:36:22 +0200 |
blanchet |
renamed experimental learning engines
|
changeset |
files
|
| Thu, 26 Jun 2014 13:36:13 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Thu, 26 Jun 2014 13:36:06 +0200 |
blanchet |
refactoring
|
changeset |
files
|
| Thu, 26 Jun 2014 13:36:00 +0200 |
blanchet |
removed experimental machine learning engine
|
changeset |
files
|
| Thu, 26 Jun 2014 13:35:56 +0200 |
blanchet |
store string-to-index tables in memory
|
changeset |
files
|
| Thu, 26 Jun 2014 13:35:52 +0200 |
blanchet |
disable 'extra' feature tainting for now
|
changeset |
files
|
| Thu, 26 Jun 2014 13:35:46 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Thu, 26 Jun 2014 13:35:39 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Thu, 26 Jun 2014 13:35:36 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Thu, 26 Jun 2014 13:35:30 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Thu, 26 Jun 2014 13:35:21 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Thu, 26 Jun 2014 13:35:17 +0200 |
blanchet |
honor visible in SML naive Bayes
|
changeset |
files
|
| Thu, 26 Jun 2014 13:35:12 +0200 |
blanchet |
honor visibility in SML k-NN
|
changeset |
files
|
| Thu, 26 Jun 2014 13:35:07 +0200 |
blanchet |
got rid of a few experimental options
|
changeset |
files
|
| Thu, 26 Jun 2014 13:35:00 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Thu, 26 Jun 2014 13:34:57 +0200 |
blanchet |
killed dead code
|
changeset |
files
|
| Thu, 26 Jun 2014 13:34:50 +0200 |
blanchet |
avoid subscripting array with ~1
|
changeset |
files
|
| Thu, 26 Jun 2014 13:34:39 +0200 |
blanchet |
killed dead data
|
changeset |
files
|
| Thu, 26 Jun 2014 13:34:28 +0200 |
blanchet |
new version of adaptive k-NN with TFIDF
|
changeset |
files
|
| Thu, 26 Jun 2014 13:33:50 +0200 |
blanchet |
refactoring
|
changeset |
files
|
| Thu, 26 Jun 2014 13:33:27 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Thu, 26 Jun 2014 13:33:21 +0200 |
blanchet |
refactoring
|
changeset |
files
|
| Thu, 26 Jun 2014 13:33:08 +0200 |
blanchet |
adaptive k-NN
|
changeset |
files
|
| Thu, 26 Jun 2014 13:33:02 +0200 |
blanchet |
avoid parallelism, since it confuses the global state and leads to cheating (with 'sml_xxx' engines)
|
changeset |
files
|
| Thu, 26 Jun 2014 13:32:56 +0200 |
blanchet |
generate right dependencies in MaSh driver
|
changeset |
files
|
| Mon, 23 Jun 2014 12:54:48 +0200 |
wenzelm |
more on "Futures";
|
changeset |
files
|
| Mon, 23 Jun 2014 12:20:20 +0200 |
wenzelm |
more on "Futures";
|
changeset |
files
|
| Sat, 21 Jun 2014 21:33:00 +0200 |
wenzelm |
more on "Future values";
|
changeset |
files
|
| Sat, 21 Jun 2014 12:19:34 +0200 |
wenzelm |
more on "Lazy evaluation";
|
changeset |
files
|
| Fri, 20 Jun 2014 20:47:22 +0200 |
wenzelm |
more on syntax phases;
|
changeset |
files
|
| Thu, 19 Jun 2014 22:07:44 +0200 |
wenzelm |
more on syntax phases;
|
changeset |
files
|
| Thu, 19 Jun 2014 21:19:30 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 19 Jun 2014 12:33:04 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 19 Jun 2014 12:05:10 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 19 Jun 2014 12:01:26 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 19 Jun 2014 11:47:46 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 18 Jun 2014 21:47:30 +0200 |
wenzelm |
added screenshot;
|
changeset |
files
|
| Wed, 18 Jun 2014 21:23:10 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 18 Jun 2014 21:17:48 +0200 |
wenzelm |
misc tuning;
|
changeset |
files
|
| Tue, 17 Jun 2014 22:18:18 +0200 |
wenzelm |
added screenshot;
|
changeset |
files
|
| Tue, 17 Jun 2014 22:00:25 +0200 |
wenzelm |
misc tuning;
|
changeset |
files
|
| Mon, 16 Jun 2014 21:26:50 +0200 |
wenzelm |
formal check of jEdit actions;
|
changeset |
files
|
| Mon, 16 Jun 2014 20:50:56 +0200 |
wenzelm |
more on "Completion";
|
changeset |
files
|
| Mon, 16 Jun 2014 14:04:48 +0200 |
wenzelm |
more on "Completion";
|
changeset |
files
|
| Mon, 16 Jun 2014 13:06:31 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 16 Jun 2014 12:52:20 +0200 |
wenzelm |
clarified role of old user interfaces as misc tools;
|
changeset |
files
|
| Mon, 16 Jun 2014 12:41:51 +0200 |
wenzelm |
added Index;
|
changeset |
files
|
| Sat, 14 Jun 2014 12:38:14 +0200 |
wenzelm |
more on "Completion";
|
changeset |
files
|
| Fri, 13 Jun 2014 22:15:13 +0200 |
wenzelm |
more on "Completion";
|
changeset |
files
|
| Fri, 13 Jun 2014 21:58:12 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 13 Jun 2014 20:01:39 +0200 |
wenzelm |
more on "Completion";
|
changeset |
files
|
| Thu, 12 Jun 2014 21:21:44 +0200 |
wenzelm |
more on "Completion";
|
changeset |
files
|
| Wed, 11 Jun 2014 22:28:24 +0200 |
wenzelm |
more on "Auxiliary files";
|
changeset |
files
|
| Wed, 11 Jun 2014 14:01:04 +0200 |
wenzelm |
more on "Document model";
|
changeset |
files
|
| Mon, 09 Jun 2014 20:44:13 +0200 |
wenzelm |
suppress index;
|
changeset |
files
|
| Mon, 09 Jun 2014 20:41:00 +0200 |
wenzelm |
more on command-line invocation -- moved material from system manual;
|
changeset |
files
|
| Mon, 09 Jun 2014 19:55:58 +0200 |
wenzelm |
clarified section structure;
|
changeset |
files
|
| Mon, 09 Jun 2014 19:43:54 +0200 |
wenzelm |
clarified section structure;
|
changeset |
files
|
| Mon, 09 Jun 2014 19:35:18 +0200 |
wenzelm |
clarified section structure;
|
changeset |
files
|
| Mon, 09 Jun 2014 12:15:53 +0200 |
wenzelm |
more on dockable windows;
|
changeset |
files
|
| Mon, 09 Jun 2014 11:05:43 +0200 |
wenzelm |
clarified section structure;
|
changeset |
files
|
| Fri, 06 Jun 2014 21:42:50 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 06 Jun 2014 21:35:23 +0200 |
wenzelm |
more on Query panel;
|
changeset |
files
|
| Fri, 06 Jun 2014 12:10:33 +0200 |
wenzelm |
updated screenshots;
|
changeset |
files
|
| Thu, 05 Jun 2014 10:54:00 +0200 |
wenzelm |
more on Query panel -- updated Find Theorems;
|
changeset |
files
|
| Wed, 04 Jun 2014 18:18:09 +0200 |
wenzelm |
misc tuning and updates;
|
changeset |
files
|
| Wed, 25 Jun 2014 07:49:21 +0200 |
Andreas Lochbihler |
merged
|
changeset |
files
|
| Tue, 24 Jun 2014 15:05:58 +0200 |
Andreas Lochbihler |
add lemma
|
changeset |
files
|
| Tue, 24 Jun 2014 15:49:20 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Tue, 24 Jun 2014 15:08:19 +0200 |
blanchet |
optimized traversal of proof terms by skipping bad apples (e.g. full_exhaustive_int'.pinduct)
|
changeset |
files
|
| Tue, 24 Jun 2014 14:56:08 +0200 |
blanchet |
minor table access optimization
|
changeset |
files
|
| Tue, 24 Jun 2014 13:48:14 +0200 |
desharna |
document property 'rel_coinduct'
|
changeset |
files
|
| Tue, 24 Jun 2014 13:48:14 +0200 |
desharna |
tune the implementation of 'rel_coinduct'
|
changeset |
files
|
| Tue, 24 Jun 2014 13:48:14 +0200 |
desharna |
generate 'rel_coinduct' theorem for codatatypes
|
changeset |
files
|
| Tue, 24 Jun 2014 13:48:14 +0200 |
desharna |
generate 'rel_coinduct0' theorem for codatatypes
|
changeset |
files
|
| Tue, 24 Jun 2014 12:36:45 +0200 |
blanchet |
added parentheses around type arguments in THF
|
changeset |
files
|
| Tue, 24 Jun 2014 12:36:45 +0200 |
blanchet |
optimize log
|
changeset |
files
|
| Tue, 24 Jun 2014 12:35:57 +0200 |
blanchet |
enable TF-IDF
|
changeset |
files
|
| Tue, 24 Jun 2014 12:35:49 +0200 |
blanchet |
added another experimental engine
|
changeset |
files
|
| Tue, 24 Jun 2014 12:35:43 +0200 |
blanchet |
tweaked experimental setup
|
changeset |
files
|
| Tue, 24 Jun 2014 08:20:00 +0200 |
blanchet |
changed order of facts so that 'name_tabs' has the same order everywhere (which affects unaliasing)
|
changeset |
files
|
| Tue, 24 Jun 2014 08:19:58 +0200 |
blanchet |
use strings to communicate with external process, to ease debugging
|
changeset |
files
|
| Tue, 24 Jun 2014 08:19:57 +0200 |
blanchet |
added 'dummy_thf_ml' prover for experiments with HOLyHammer
|
changeset |
files
|
| Tue, 24 Jun 2014 08:19:56 +0200 |
blanchet |
phantoms may also occur in THF1
|
changeset |
files
|
| Tue, 24 Jun 2014 08:19:55 +0200 |
blanchet |
added experimental MaSh engine
|
changeset |
files
|
| Tue, 24 Jun 2014 08:19:55 +0200 |
blanchet |
move method silencing code closer to the methods it is trying to silence, to reduce bad side-effects
|
changeset |
files
|
| Tue, 24 Jun 2014 08:19:54 +0200 |
blanchet |
help reconstruction of Z3 skolemization by weakening formulas a bit
|
changeset |
files
|
| Tue, 24 Jun 2014 08:19:22 +0200 |
blanchet |
supports gradual skolemization (cf. Z3) by threading context through correctly
|
changeset |
files
|