| Wed, 10 Nov 2010 20:21:55 +0100 |
wenzelm |
added buffer_text convenience, with explicit locking;
|
changeset |
files
|
| Wed, 10 Nov 2010 17:53:41 +0100 |
wenzelm |
use official/portable Multithreading.max_threads_value, which is also subject to user preferences (NB: Thread.numProcessors is apt to lead to surprises like very high numbers for systems with hyperthreading);
|
changeset |
files
|
| Wed, 10 Nov 2010 16:05:15 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 10 Nov 2010 09:03:07 +0100 |
blanchet |
make SML/NJ happy
|
changeset |
files
|
| Tue, 09 Nov 2010 16:18:40 +0100 |
haftmann |
merged
|
changeset |
files
|
| Tue, 09 Nov 2010 14:02:14 +0100 |
haftmann |
slightly changed fun_map_def
|
changeset |
files
|
| Tue, 09 Nov 2010 14:02:14 +0100 |
haftmann |
fun_rel_def is no simp rule by default
|
changeset |
files
|
| Tue, 09 Nov 2010 14:02:13 +0100 |
haftmann |
more appropriate specification packages; fun_rel_def is no simp rule by default
|
changeset |
files
|
| Tue, 09 Nov 2010 14:02:13 +0100 |
haftmann |
type annotations in specifications; fun_rel_def is no simp rule by default; slightly changed fun_map_def; more on predicates on relation functions; proper HOL equations in definitions
|
changeset |
files
|
| Tue, 09 Nov 2010 14:02:13 +0100 |
haftmann |
more appropriate specification packages; fun_rel_def is no simp rule by default
|
changeset |
files
|
| Tue, 09 Nov 2010 14:02:12 +0100 |
haftmann |
type annotations in specifications; fun_rel_def is no simp rule by default
|
changeset |
files
|
| Tue, 09 Nov 2010 14:02:12 +0100 |
haftmann |
fun_rel_def is no simp rule by default
|
changeset |
files
|
| Tue, 09 Nov 2010 14:00:10 +0000 |
paulson |
merged
|
changeset |
files
|
| Tue, 09 Nov 2010 13:59:37 +0000 |
paulson |
tidied using metis
|
changeset |
files
|
| Wed, 10 Nov 2010 15:59:23 +0100 |
wenzelm |
manage folding via sidekick by default;
|
changeset |
files
|
| Wed, 10 Nov 2010 15:47:56 +0100 |
wenzelm |
eliminated obsolete heading category -- superseded by heading_level;
|
changeset |
files
|
| Wed, 10 Nov 2010 15:43:06 +0100 |
wenzelm |
treat main theory commands like headings, and nest anything else inside;
|
changeset |
files
|
| Wed, 10 Nov 2010 15:42:20 +0100 |
wenzelm |
proper treatment of equal heading level;
|
changeset |
files
|
| Wed, 10 Nov 2010 15:41:29 +0100 |
wenzelm |
added missing Keyword.THY_SCHEMATIC_GOAL;
|
changeset |
files
|
| Wed, 10 Nov 2010 15:17:25 +0100 |
wenzelm |
default Sidekick parser based on section headings;
|
changeset |
files
|
| Wed, 10 Nov 2010 15:00:40 +0100 |
wenzelm |
some support for nested source structure, based on section headings;
|
changeset |
files
|
| Wed, 10 Nov 2010 11:44:35 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 09 Nov 2010 23:24:46 +0100 |
wenzelm |
misc tuning and simplification, using Isabelle_Sidekick.Asset (not sidekick.Asset, which is dynamically dispatched to slightly different semantics);
|
changeset |
files
|
| Tue, 09 Nov 2010 22:37:10 +0100 |
wenzelm |
updated version;
|
changeset |
files
|
| Tue, 09 Nov 2010 21:52:05 +0100 |
wenzelm |
private counter, to keep externalized ids a bit smaller;
|
changeset |
files
|
| Tue, 09 Nov 2010 21:44:19 +0100 |
wenzelm |
added general Synchronized.counter convenience;
|
changeset |
files
|
| Tue, 09 Nov 2010 21:13:06 +0100 |
wenzelm |
explicitly identify forked/joined tasks;
|
changeset |
files
|
| Tue, 09 Nov 2010 11:27:58 +0100 |
wenzelm |
accomodate old manuals that include pdfsetup.sty without isabelle.sty;
|
changeset |
files
|
| Tue, 09 Nov 2010 11:17:15 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 08 Nov 2010 23:02:20 +0100 |
krauss |
removed type-inference-like behaviour from relation_tac completely; tuned
|
changeset |
files
|
| Mon, 08 Nov 2010 20:55:27 +0100 |
wenzelm |
avoid clash of \<upharpoonright> vs. \<restriction> (cf. 666ea7e62384 and 3c49dbece0a8);
|
changeset |
files
|
| Mon, 08 Nov 2010 20:50:56 +0100 |
wenzelm |
explicitly check uniqueness of symbol recoding;
|
changeset |
files
|
| Mon, 08 Nov 2010 17:44:47 +0100 |
wenzelm |
more hints on building and running Isabelle/jEdit from command line;
|
changeset |
files
|
| Mon, 08 Nov 2010 14:41:11 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 08 Nov 2010 14:33:54 +0100 |
blanchet |
merge
|
changeset |
files
|
| Mon, 08 Nov 2010 14:33:30 +0100 |
blanchet |
reduce the number of monomorphization iterations from 10 (the default) to 4, in the interest of faster SMT solving
|
changeset |
files
|
| Mon, 08 Nov 2010 05:07:18 -0800 |
huffman |
merged
|
changeset |
files
|
| Sat, 06 Nov 2010 10:01:00 -0700 |
huffman |
merged
|
changeset |
files
|
| Fri, 05 Nov 2010 15:15:28 -0700 |
huffman |
(infixl "<<" 55) -> (infix "<<" 50)
|
changeset |
files
|
| Wed, 03 Nov 2010 17:22:25 -0700 |
huffman |
simplify some proofs
|
changeset |
files
|
| Wed, 03 Nov 2010 17:06:21 -0700 |
huffman |
remove unnecessary stuff from Discrete.thy
|
changeset |
files
|
| Wed, 03 Nov 2010 16:39:23 -0700 |
huffman |
remove some unnecessary lemmas; move monofun_LAM to Cfun.thy
|
changeset |
files
|
| Wed, 03 Nov 2010 15:57:39 -0700 |
huffman |
add lemma eq_imp_below
|
changeset |
files
|
| Wed, 03 Nov 2010 15:47:46 -0700 |
huffman |
discontinue a bunch of legacy theorem names
|
changeset |
files
|
| Wed, 03 Nov 2010 15:31:24 -0700 |
huffman |
move a few admissibility lemmas into FOCUS/Stream_adm.thy
|
changeset |
files
|
| Wed, 03 Nov 2010 15:03:16 -0700 |
huffman |
simplify some proofs
|
changeset |
files
|
| Mon, 08 Nov 2010 13:53:18 +0100 |
blanchet |
compile -- 7550b2cba1cb broke the build
|
changeset |
files
|
| Mon, 08 Nov 2010 13:25:00 +0100 |
blanchet |
merge
|
changeset |
files
|
| Mon, 08 Nov 2010 09:10:44 +0100 |
blanchet |
recognize Vampire error
|
changeset |
files
|
| Mon, 08 Nov 2010 12:13:51 +0100 |
boehmes |
return the process return code along with the process outputs
|
changeset |
files
|
| Mon, 08 Nov 2010 12:13:44 +0100 |
boehmes |
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
|
changeset |
files
|
| Mon, 08 Nov 2010 11:49:28 +0100 |
haftmann |
merged
|
changeset |
files
|
| Mon, 08 Nov 2010 10:56:48 +0100 |
haftmann |
corrected slip: must keep constant map, not type map; tuned code
|
changeset |
files
|
| Mon, 08 Nov 2010 10:43:24 +0100 |
haftmann |
constructors to datatypes in code_reflect can be globbed; dropped unused code
|
changeset |
files
|
| Mon, 08 Nov 2010 09:25:43 +0100 |
bulwahn |
adding code and theory for smallvalue generators, but do not setup the interpretation yet
|
changeset |
files
|
| Mon, 08 Nov 2010 02:33:48 +0100 |
blanchet |
make sure the SMT solver runs several iterations by lowering the timeout at each iteration -- yields better results in practice
|
changeset |
files
|
| Mon, 08 Nov 2010 02:32:27 +0100 |
blanchet |
better detection of completely irrelevant facts
|
changeset |
files
|
| Sun, 07 Nov 2010 18:19:04 +0100 |
blanchet |
always use a hard timeout in Mirabelle
|
changeset |
files
|
| Sun, 07 Nov 2010 18:15:13 +0100 |
blanchet |
use "smt" (rather than "metis") to reconstruct SMT proofs
|
changeset |
files
|
| Sun, 07 Nov 2010 18:03:24 +0100 |
blanchet |
don't pass too many facts on the first iteration of the SMT solver
|
changeset |
files
|
| Sun, 07 Nov 2010 18:02:02 +0100 |
blanchet |
catch TimeOut exception
|
changeset |
files
|
| Sun, 07 Nov 2010 17:56:07 +0100 |
blanchet |
ensure the SMT solver respects the timeout -- Mirabelle revealed cases where "smt_filter" apparently never returns
|
changeset |
files
|
| Sun, 07 Nov 2010 17:51:25 +0100 |
blanchet |
if SMT used as a filter in a loop fails at each iteration, returns the first error, not the last, since it is more informative -- the first error typically says "out of memory", whereas the last might well be "the SMT problem is unprovable", which should be no surprise if too many facts were removed
|
changeset |
files
|
| Sun, 07 Nov 2010 13:29:59 +0100 |
blanchet |
removed explicit "Interrupt" handling for conformity with async model -- unfortunately the user loses the information about how many scopes were checked, but this needs to be retought with the new interface anyway
|
changeset |
files
|
| Sat, 06 Nov 2010 10:25:08 +0100 |
blanchet |
make Nitpick datatype tests faster to make timeout less likely
|
changeset |
files
|
| Sat, 06 Nov 2010 10:25:08 +0100 |
blanchet |
invoke SMT solver in a loop, with fewer and fewer facts, in case of error
|
changeset |
files
|
| Sat, 06 Nov 2010 10:25:08 +0100 |
blanchet |
always honor the max relevant constraint
|
changeset |
files
|
| Mon, 08 Nov 2010 11:28:22 +0100 |
wenzelm |
more robust treatment of suppressed quotes concerning replacement text -- for improved copy/paste behaviour;
|
changeset |
files
|
| Mon, 08 Nov 2010 00:00:47 +0100 |
wenzelm |
updated generated files;
|
changeset |
files
|
| Sun, 07 Nov 2010 23:32:26 +0100 |
wenzelm |
tweaked pdf setup to allow modification of \pdfminorversion;
|
changeset |
files
|
| Sun, 07 Nov 2010 23:12:40 +0100 |
wenzelm |
merged;
|
changeset |
files
|
| Sun, 07 Nov 2010 23:12:21 +0100 |
wenzelm |
updated generated files;
|
changeset |
files
|
| Sun, 07 Nov 2010 22:51:16 +0100 |
wenzelm |
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
|
changeset |
files
|
| Sun, 07 Nov 2010 22:42:49 +0100 |
wenzelm |
updated generated file;
|
changeset |
files
|
| Sun, 07 Nov 2010 22:26:25 +0100 |
wenzelm |
more literal appearance of antiqopen/antiqclose;
|
changeset |
files
|
| Sun, 07 Nov 2010 16:39:03 +0100 |
wenzelm |
'example_proof' is treated as non-schematic statement with irrelevant proof (NB: even regular proofs can contain unreachable parts wrt. the graph of proof promises);
|
changeset |
files
|
| Sat, 06 Nov 2010 20:59:59 +0100 |
wenzelm |
continue after failed commands;
|
changeset |
files
|
| Sat, 06 Nov 2010 20:18:06 +0100 |
wenzelm |
added Keyword.is_heading (cf. Scala version);
|
changeset |
files
|
| Sat, 06 Nov 2010 19:37:31 +0100 |
wenzelm |
updated keywords;
|
changeset |
files
|
| Sat, 06 Nov 2010 19:36:54 +0100 |
wenzelm |
mark 'cd' and 'commit' as control command -- not usable in asynchronous document model, likely to cause confusion in Proof General;
|
changeset |
files
|
| Sat, 06 Nov 2010 18:10:35 +0100 |
wenzelm |
somewhat more uniform timing markup in ML vs. Scala;
|
changeset |
files
|
| Sat, 06 Nov 2010 17:55:32 +0100 |
wenzelm |
somewhat more uniform timing in ML vs. Scala;
|
changeset |
files
|
| Sat, 06 Nov 2010 16:53:07 +0100 |
wenzelm |
added Markup.Double, Markup.Double_Property;
|
changeset |
files
|
| Sat, 06 Nov 2010 16:31:35 +0100 |
wenzelm |
explicit "timing" status for toplevel transactions;
|
changeset |
files
|
| Sat, 06 Nov 2010 16:03:49 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 06 Nov 2010 15:34:11 +0100 |
wenzelm |
tuned comments;
|
changeset |
files
|
| Sat, 06 Nov 2010 00:10:32 +0100 |
krauss |
abolished obscure goal variant of [split_format] -- unused (cf. d1c14898fd04), unrelated to '(complete)' variant, and not at all canonical
|
changeset |
files
|
| Fri, 05 Nov 2010 23:19:20 +0100 |
wenzelm |
moved ISABELLE_IDENTIFIER from ISABELLE_OUTPUT further up to ISABELLE_HOME_USER;
|
changeset |
files
|
| Fri, 05 Nov 2010 22:03:57 +0100 |
wenzelm |
updated keywords;
|
changeset |
files
|
| Fri, 05 Nov 2010 22:01:01 +0100 |
wenzelm |
reflect actual content of /home/isabelle/.html-data/cgi-bin/hgwebdir.cgi;
|
changeset |
files
|
| Fri, 05 Nov 2010 21:53:25 +0100 |
wenzelm |
eliminated spurious "firstline" filters for improved display of Isabelle history logs: one item per line, without special headline;
|
changeset |
files
|
| Fri, 05 Nov 2010 21:48:48 +0100 |
wenzelm |
reflect actual content of /home/isabelle-repository/hgweb-templates/isabelle by krauss;
|
changeset |
files
|
| Fri, 05 Nov 2010 21:42:32 +0100 |
wenzelm |
obsolete -- python installation on www4 is not modified (despite remaining "firstline" in graph and syndication views);
|
changeset |
files
|
| Fri, 05 Nov 2010 19:47:20 +0100 |
wenzelm |
explicit indication of some remaining violations of the Isabelle/ML interrupt model;
|
changeset |
files
|
| Fri, 05 Nov 2010 19:39:25 +0100 |
wenzelm |
updated generated file, overwriting 55a1693affb6 whose content appears to be in the thy source already;
|
changeset |
files
|
| Fri, 05 Nov 2010 19:22:04 +0100 |
wenzelm |
proper spelling;
|
changeset |
files
|
| Fri, 05 Nov 2010 15:09:55 +0100 |
hoelzl |
merged
|
changeset |
files
|
| Fri, 05 Nov 2010 14:17:18 +0100 |
hoelzl |
Extend convex analysis by Bogdan Grechuk
|
changeset |
files
|
| Fri, 05 Nov 2010 14:36:17 +0100 |
blanchet |
merged
|
changeset |
files
|
| Fri, 05 Nov 2010 09:49:03 +0100 |
blanchet |
fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
|
changeset |
files
|
| Fri, 05 Nov 2010 09:05:22 +0100 |
blanchet |
make Mirabelle work correctly if the prover (e.g. the SMT solver) returns no timing information
|
changeset |
files
|
| Thu, 04 Nov 2010 15:31:26 +0100 |
blanchet |
pass proper type to SMT_Builtin.is_builtin
|
changeset |
files
|
| Thu, 04 Nov 2010 15:30:48 +0100 |
blanchet |
remove " s" suffix since seconds are now implicit
|
changeset |
files
|
| Thu, 04 Nov 2010 14:59:44 +0100 |
blanchet |
ignore facts with only theory constants in them
|
changeset |
files
|
| Thu, 04 Nov 2010 14:59:44 +0100 |
blanchet |
cosmetics
|
changeset |
files
|
| Thu, 04 Nov 2010 14:59:44 +0100 |
blanchet |
use the SMT integration's official list of built-ins
|
changeset |
files
|
| Fri, 05 Nov 2010 14:10:41 +0100 |
haftmann |
added class relation group_add < cancel_semigroup_add
|
changeset |
files
|
| Fri, 05 Nov 2010 09:07:14 +0100 |
bulwahn |
merged
|
changeset |
files
|
| Fri, 05 Nov 2010 08:16:35 +0100 |
bulwahn |
changing timeout to real value; handling Interrupt and Timeout more like nitpick does
|
changeset |
files
|
| Fri, 05 Nov 2010 08:16:34 +0100 |
bulwahn |
added two lemmas about injectivity of concat to the list theory
|
changeset |
files
|
| Fri, 05 Nov 2010 08:16:31 +0100 |
bulwahn |
adding documentation of some quickcheck options
|
changeset |
files
|
| Fri, 05 Nov 2010 08:28:57 +0100 |
haftmann |
merged
|
changeset |
files
|
| Thu, 04 Nov 2010 17:27:38 +0100 |
haftmann |
Code.check_const etc.: reject too specific types
|
changeset |
files
|
| Thu, 04 Nov 2010 17:27:37 +0100 |
haftmann |
corrected quoting
|
changeset |
files
|
| Thu, 04 Nov 2010 17:27:37 +0100 |
haftmann |
added lemma length_alloc
|
changeset |
files
|
| Thu, 04 Nov 2010 13:42:36 +0100 |
haftmann |
dropped return abbreviation for Pair -- confusing if combined with monad syntax; tuned document
|
changeset |
files
|
| Thu, 04 Nov 2010 13:42:36 +0100 |
haftmann |
added note on countable types
|
changeset |
files
|
| Thu, 04 Nov 2010 18:01:55 +0100 |
boehmes |
simulate more closely the behaviour of the tactic
|
changeset |
files
|
| Thu, 04 Nov 2010 17:17:21 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 04 Nov 2010 13:37:11 +0100 |
haftmann |
merged
|
changeset |
files
|