| Wed, 28 Nov 2012 12:25:43 +0100 |
smolkas |
added signature
|
changeset |
files
|
| Wed, 28 Nov 2012 12:25:43 +0100 |
smolkas |
moved thms_of_name to Sledgehammer_Util and removed copies, updated references
|
changeset |
files
|
| Wed, 28 Nov 2012 12:25:43 +0100 |
smolkas |
removed duplicate decleration
|
changeset |
files
|
| Wed, 28 Nov 2012 12:25:43 +0100 |
smolkas |
made use of sledgehammer_util
|
changeset |
files
|
| Wed, 28 Nov 2012 12:25:43 +0100 |
smolkas |
renamed sledgehammer_isar_reconstruct to sledgehammer_proof
|
changeset |
files
|
| Wed, 28 Nov 2012 12:25:43 +0100 |
smolkas |
added comments to new source files
|
changeset |
files
|
| Wed, 28 Nov 2012 12:25:43 +0100 |
smolkas |
fixed problem with fact names
|
changeset |
files
|
| Wed, 28 Nov 2012 12:25:06 +0100 |
smolkas |
remove hack and generalize code slightly
|
changeset |
files
|
| Wed, 28 Nov 2012 12:23:44 +0100 |
smolkas |
simplified isar_qualifiers and qs merging
|
changeset |
files
|
| Wed, 28 Nov 2012 12:22:17 +0100 |
smolkas |
put shrink in own structure
|
changeset |
files
|
| Wed, 28 Nov 2012 12:22:05 +0100 |
smolkas |
put annotate in own structure
|
changeset |
files
|
| Wed, 28 Nov 2012 12:21:42 +0100 |
smolkas |
support assumptions as facts for preplaying
|
changeset |
files
|
| Wed, 28 Nov 2012 12:20:06 +0100 |
smolkas |
some minor improvements in shrink_proof
|
changeset |
files
|
| Wed, 28 Nov 2012 17:18:53 +0100 |
wenzelm |
some support for ML runtime statistics;
|
changeset |
files
|
| Wed, 28 Nov 2012 16:09:05 +0100 |
wenzelm |
prefer tight Markup.print_int/parse_int for property values;
|
changeset |
files
|
| Wed, 28 Nov 2012 16:07:17 +0100 |
wenzelm |
clarified new identifier syntax: exclude \<^isup>, include subscripted prime (to allow imitating full identifier here);
|
changeset |
files
|
| Wed, 28 Nov 2012 15:59:18 +0100 |
wenzelm |
eliminated slightly odd identifiers;
|
changeset |
files
|
| Wed, 28 Nov 2012 15:38:12 +0100 |
wenzelm |
tuned syntax, potentially more robust;
|
changeset |
files
|
| Wed, 28 Nov 2012 14:55:46 +0100 |
wenzelm |
smarter list layout;
|
changeset |
files
|
| Tue, 27 Nov 2012 20:01:57 +0100 |
wenzelm |
repaired text following 491c5c81c2e8;
|
changeset |
files
|
| Tue, 27 Nov 2012 19:43:00 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 27 Nov 2012 19:31:11 +0100 |
hoelzl |
introduce filter_lim as a generatlization of tendsto
|
changeset |
files
|
| Tue, 27 Nov 2012 19:24:30 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 27 Nov 2012 13:48:40 +0100 |
immler |
based countable topological basis on Countable_Set
|
changeset |
files
|
| Tue, 27 Nov 2012 11:29:47 +0100 |
immler |
qualified interpretation of sigma_algebra, to avoid name clashes
|
changeset |
files
|
| Thu, 22 Nov 2012 10:09:54 +0100 |
immler |
eliminated finite_set_sequence with countable set
|
changeset |
files
|
| Tue, 27 Nov 2012 19:22:36 +0100 |
wenzelm |
support for sub-structured identifier syntax (inactive);
|
changeset |
files
|
| Tue, 27 Nov 2012 13:22:29 +0100 |
wenzelm |
eliminated some improper identifiers;
|
changeset |
files
|
| Tue, 27 Nov 2012 10:56:31 +0100 |
hoelzl |
add upper bounds for factorial and binomial; add equation for binomial using nat-division (both from AFP/Girth_Chromatic)
|
changeset |
files
|
| Mon, 26 Nov 2012 21:46:04 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Mon, 26 Nov 2012 21:10:42 +0100 |
wenzelm |
more uniform Symbol.is_ascii_identifier in ML/Scala;
|
changeset |
files
|
| Mon, 26 Nov 2012 20:58:41 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 26 Nov 2012 20:39:19 +0100 |
wenzelm |
clarified Symbol.scan_ascii_id;
|
changeset |
files
|
| Mon, 26 Nov 2012 20:29:40 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 26 Nov 2012 20:09:51 +0100 |
wenzelm |
convenience operations for table as set;
|
changeset |
files
|
| Mon, 26 Nov 2012 19:56:09 +0100 |
wenzelm |
removed remains of Oheimb's double-space (cf. 0a5af667dc75);
|
changeset |
files
|
| Mon, 26 Nov 2012 19:53:43 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 26 Nov 2012 17:13:44 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 26 Nov 2012 16:01:04 +0100 |
blanchet |
updated two components
|
changeset |
files
|
| Mon, 26 Nov 2012 15:31:03 +0100 |
blanchet |
simplify code slightly
|
changeset |
files
|
| Mon, 26 Nov 2012 15:31:03 +0100 |
blanchet |
avoid non-ASCII sign
|
changeset |
files
|
| Mon, 26 Nov 2012 14:20:51 +0100 |
kuncar |
generate a parameterized correspondence relation
|
changeset |
files
|
| Mon, 26 Nov 2012 14:20:36 +0100 |
kuncar |
quot_thm_crel
|
changeset |
files
|
| Mon, 26 Nov 2012 14:15:48 +0100 |
kuncar |
add option_fold
|
changeset |
files
|
| Mon, 26 Nov 2012 14:11:31 +0100 |
hoelzl |
add binomial_ge_n_over_k_pow_k
|
changeset |
files
|
| Mon, 26 Nov 2012 13:50:25 +0100 |
blanchet |
removed tool that was never finished
|
changeset |
files
|
| Mon, 26 Nov 2012 13:35:05 +0100 |
blanchet |
added file headers
|
changeset |
files
|
| Mon, 26 Nov 2012 12:13:37 +0100 |
blanchet |
updated MaSh doc
|
changeset |
files
|
| Mon, 26 Nov 2012 12:04:32 +0100 |
blanchet |
moved MaSh's Python code into Isabelle
|
changeset |
files
|
| Mon, 26 Nov 2012 11:46:19 +0100 |
blanchet |
updated NEWS etc.
|
changeset |
files
|
| Mon, 26 Nov 2012 11:45:12 +0100 |
blanchet |
distinguish declated tfrees from other tfrees -- only the later can be optimized away
|
changeset |
files
|
| Mon, 26 Nov 2012 16:28:22 +0100 |
wenzelm |
clarified status of Legacy_XML_Syntax, despite lack of Proofterm_XML;
|
changeset |
files
|
| Mon, 26 Nov 2012 16:22:29 +0100 |
wenzelm |
reset active areas on content update;
|
changeset |
files
|
| Mon, 26 Nov 2012 16:16:47 +0100 |
wenzelm |
more general sendback properties;
|
changeset |
files
|
| Mon, 26 Nov 2012 14:43:28 +0100 |
wenzelm |
tuned command descriptions;
|
changeset |
files
|
| Mon, 26 Nov 2012 13:54:43 +0100 |
wenzelm |
refined outer syntax 'help' command;
|
changeset |
files
|
| Mon, 26 Nov 2012 11:59:56 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Mon, 26 Nov 2012 11:42:16 +0100 |
wenzelm |
always reset active areas;
|
changeset |
files
|
| Mon, 26 Nov 2012 10:37:05 +0100 |
wenzelm |
no special treatment of control_reset, in accordance to other control styles;
|
changeset |
files
|
| Sun, 25 Nov 2012 21:40:34 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Sun, 25 Nov 2012 21:35:29 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Sun, 25 Nov 2012 21:23:20 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Sun, 25 Nov 2012 21:10:29 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Sun, 25 Nov 2012 20:59:32 +0100 |
wenzelm |
renamed main plugin object to PIDE;
|
changeset |
files
|
| Sun, 25 Nov 2012 20:31:49 +0100 |
wenzelm |
tuned signature -- avoid intrusion of module Path in generic PIDE concepts;
|
changeset |
files
|
| Sun, 25 Nov 2012 20:17:04 +0100 |
wenzelm |
explicit module UTF8;
|
changeset |
files
|
| Sun, 25 Nov 2012 19:55:42 +0100 |
wenzelm |
tuned file name;
|
changeset |
files
|
| Sun, 25 Nov 2012 19:49:24 +0100 |
wenzelm |
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
|
changeset |
files
|
| Sun, 25 Nov 2012 18:50:13 +0100 |
wenzelm |
prefer strict error;
|
changeset |
files
|
| Sun, 25 Nov 2012 18:47:33 +0100 |
wenzelm |
quasi-abstract module Rendering, with Isabelle-specific implementation;
|
changeset |
files
|
| Sun, 25 Nov 2012 17:15:21 +0100 |
wenzelm |
added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
|
changeset |
files
|
| Sun, 25 Nov 2012 15:17:01 +0100 |
wenzelm |
eval PDF_VIEWER/DVI_VIEWER command line, which allows additional quotes for program name, for example;
|
changeset |
files
|
| Sat, 24 Nov 2012 19:56:44 +0100 |
wenzelm |
retain hidden_color (i.e. transparent white) instead of replacing it by semantic text color, to make control symbols more hidden and avoid "dirty" lines with some fonts;
|
changeset |
files
|
| Sat, 24 Nov 2012 19:01:08 +0100 |
wenzelm |
prefer buffer_edit combinator over Java-style boilerplate;
|
changeset |
files
|
| Sat, 24 Nov 2012 18:34:47 +0100 |
wenzelm |
more robust font for control symbols, to ensure these obscure codepoints are properly rendered;
|
changeset |
files
|
| Sat, 24 Nov 2012 18:32:05 +0100 |
wenzelm |
tuned symbol groups;
|
changeset |
files
|
| Sat, 24 Nov 2012 18:29:19 +0100 |
wenzelm |
tuned -- Symbol.groups already sorted;
|
changeset |
files
|
| Sat, 24 Nov 2012 17:46:54 +0100 |
wenzelm |
more robust default font -- user might have switched jEdit TextArea to another font that lacks glyphs;
|
changeset |
files
|
| Sat, 24 Nov 2012 17:12:06 +0100 |
wenzelm |
added option jedit_symbols_search_limit;
|
changeset |
files
|
| Sat, 24 Nov 2012 17:05:10 +0100 |
wenzelm |
avoid empty tooltip;
|
changeset |
files
|
| Sat, 24 Nov 2012 16:59:07 +0100 |
wenzelm |
tuned symbol groups;
|
changeset |
files
|
| Sat, 24 Nov 2012 16:40:42 +0100 |
wenzelm |
special handling of control symbols in Symbols dockable;
|
changeset |
files
|
| Sat, 24 Nov 2012 16:24:39 +0100 |
wenzelm |
recovered some tooltip wrapping from e2762f962042, with multi-line support via HTML.encode;
|
changeset |
files
|
| Sat, 24 Nov 2012 16:13:21 +0100 |
wenzelm |
avoid showing semantic aspects of Unicode -- Isabelle/Scala merely (ab)uses the low-level rendering model (codepoint + font);
|
changeset |
files
|
| Sat, 24 Nov 2012 15:49:43 +0100 |
wenzelm |
more NEWS/CONTRIBUTORS;
|
changeset |
files
|
| Sat, 24 Nov 2012 14:50:19 +0100 |
wenzelm |
improved editing support for control styles;
|
changeset |
files
|
| Sat, 24 Nov 2012 12:39:58 +0100 |
wenzelm |
added ISABELLE_PLATFORM_FAMILY;
|
changeset |
files
|
| Fri, 23 Nov 2012 23:07:58 +0100 |
nipkow |
merged
|
changeset |
files
|
| Fri, 23 Nov 2012 23:07:38 +0100 |
nipkow |
moved lemma
|
changeset |
files
|
| Fri, 23 Nov 2012 22:16:52 +0100 |
wenzelm |
timeout in proper place (HOL-Quickcheck_Examples approx. 1min, HOL-Quickcheck_Benchmark approx. 1h);
|
changeset |
files
|
| Fri, 23 Nov 2012 18:28:00 +0100 |
hoelzl |
add quotient_of_div
|
changeset |
files
|
| Fri, 23 Nov 2012 17:24:12 +0100 |
kuncar |
generate correct names
|
changeset |
files
|
| Fri, 23 Nov 2012 15:53:24 +0100 |
kuncar |
simplified code
|
changeset |
files
|
| Fri, 23 Nov 2012 15:53:19 +0100 |
kuncar |
generate correct correspondence relation name
|
changeset |
files
|
| Fri, 23 Nov 2012 15:08:44 +0100 |
wenzelm |
more uniform title, follow-up to 928cb8b35e6e;
|
changeset |
files
|
| Fri, 23 Nov 2012 13:46:01 +0100 |
nipkow |
tuned
|
changeset |
files
|
| Thu, 22 Nov 2012 22:21:54 +0100 |
wenzelm |
defer interpretation of markup via implicit print mode;
|
changeset |
files
|
| Thu, 22 Nov 2012 17:26:06 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 22 Nov 2012 14:44:37 +0100 |
traytel |
made SML/NJ happier
|
changeset |
files
|
| Thu, 22 Nov 2012 17:11:26 +0100 |
wenzelm |
pack window before accessing its geometry;
|
changeset |
files
|
| Thu, 22 Nov 2012 17:01:20 +0100 |
wenzelm |
always refresh font metrics, to help window size calculation (amending 2585c81d840a);
|
changeset |
files
|
| Thu, 22 Nov 2012 16:55:53 +0100 |
wenzelm |
more precise tooltip window size;
|
changeset |
files
|
| Thu, 22 Nov 2012 15:22:27 +0100 |
wenzelm |
take component width as indication if it is already visible/layed-out, to avoid multiple formatting with minimal margin;
|
changeset |
files
|
| Thu, 22 Nov 2012 14:53:02 +0100 |
wenzelm |
reset active area for outdated snapshot (again?);
|
changeset |
files
|
| Thu, 22 Nov 2012 14:40:39 +0100 |
wenzelm |
some support for implicit senback, meaning that it uses the caret position instead of explicit command exec_id;
|
changeset |
files
|
| Thu, 22 Nov 2012 13:21:02 +0100 |
wenzelm |
more abstract Sendback operations, with explicit id/exec_id properties;
|
changeset |
files
|
| Thu, 22 Nov 2012 12:22:03 +0100 |
wenzelm |
some support for breakable text and paragraphs;
|
changeset |
files
|
| Thu, 22 Nov 2012 08:23:13 +0100 |
nipkow |
tuned names
|
changeset |
files
|
| Wed, 21 Nov 2012 21:08:20 +0100 |
wenzelm |
tuned comment;
|
changeset |
files
|
| Wed, 21 Nov 2012 20:50:34 +0100 |
wenzelm |
clarified symbol groups, despite this traditional arrangement in X-symbol grid;
|
changeset |
files
|
| Wed, 21 Nov 2012 20:36:52 +0100 |
wenzelm |
always retain message positions, in order to allow Isabelle_Rendering.sendback retrieve the exec_id, even in tooltip or detached window;
|
changeset |
files
|
| Wed, 21 Nov 2012 20:15:25 +0100 |
wenzelm |
tuned whitespace;
|
changeset |
files
|
| Wed, 21 Nov 2012 16:43:14 +0100 |
immler |
merged
|
changeset |
files
|
| Wed, 21 Nov 2012 16:32:34 +0100 |
immler |
included abbrev in tooltip
|
changeset |
files
|
| Wed, 21 Nov 2012 16:21:16 +0100 |
immler |
removed (unicode) tooltips: can not adjust font in basic swing tooltip
|
changeset |
files
|
| Wed, 21 Nov 2012 16:04:00 +0100 |
immler |
delayed search to improve reactivity
|
changeset |
files
|
| Wed, 21 Nov 2012 14:53:26 +0100 |
immler |
respect font property for symbols
|
changeset |
files
|
| Wed, 21 Nov 2012 12:11:21 +0100 |
immler |
capitalize lowercase groups;
|
changeset |
files
|
| Wed, 21 Nov 2012 15:52:44 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 21 Nov 2012 15:50:54 +0100 |
wenzelm |
more generous timeout for SML/NJ, which is approx. 40-80 times slower than Poly/ML;
|
changeset |
files
|
| Wed, 21 Nov 2012 15:47:55 +0100 |
hoelzl |
Countable_Set: tuned lemma names; more generic lemmas
|
changeset |
files
|
| Wed, 21 Nov 2012 14:07:35 +0100 |
wenzelm |
enable Symbols dockable by default;
|
changeset |
files
|
| Wed, 21 Nov 2012 14:06:59 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 21 Nov 2012 13:47:47 +0100 |
wenzelm |
accomodate scala-2.10.0-RC2 with its slight reform on for-syntax;
|
changeset |
files
|
| Wed, 21 Nov 2012 12:05:05 +0100 |
hoelzl |
renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
|
changeset |
files
|
| Wed, 21 Nov 2012 10:51:12 +0100 |
immler |
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
|
changeset |
files
|
| Wed, 21 Nov 2012 11:08:56 +0100 |
hoelzl |
CONTRIBUTION: add fabians work
|
changeset |
files
|
| Wed, 21 Nov 2012 10:57:50 +0100 |
hoelzl |
NEWS: document changes in HOL-Probability
|
changeset |
files
|
| Wed, 21 Nov 2012 10:48:58 +0100 |
hoelzl |
NEWS (changeset 13211e07d931): add Countable_Set
|
changeset |
files
|
| Wed, 21 Nov 2012 10:48:22 +0100 |
hoelzl |
NEWS (changeset 69b35a75caf3): document changes in FuncSet
|
changeset |
files
|
| Wed, 21 Nov 2012 09:07:41 +0100 |
nipkow |
new theory of immutable arrays
|
changeset |
files
|
| Tue, 20 Nov 2012 22:53:59 +0100 |
wenzelm |
some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
|
changeset |
files
|
| Tue, 20 Nov 2012 22:52:04 +0100 |
wenzelm |
support for symbol groups, retaining original order of declarations;
|
changeset |
files
|
| Tue, 20 Nov 2012 21:01:53 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 20 Nov 2012 18:59:35 +0100 |
hoelzl |
add Countable_Set theory
|
changeset |
files
|
| Tue, 20 Nov 2012 17:49:26 +0100 |
nipkow |
tuned proof
|
changeset |
files
|
| Tue, 20 Nov 2012 15:18:11 +0100 |
wenzelm |
simplified command line of "isabelle install";
|
changeset |
files
|
| Tue, 20 Nov 2012 14:55:52 +0100 |
wenzelm |
known problems with Mac OS X are back -- Java 7u6 is not the last word (cf. ce37d4f8b4f4);
|
changeset |
files
|
| Tue, 20 Nov 2012 14:29:46 +0100 |
wenzelm |
some documentation for "algebra" in HOL;
|
changeset |
files
|
| Tue, 20 Nov 2012 13:27:24 +0100 |
wenzelm |
global default for session timeout;
|
changeset |
files
|
| Mon, 19 Nov 2012 22:34:17 +0100 |
wenzelm |
alternative completion for outer syntax keywords;
|
changeset |
files
|
| Mon, 19 Nov 2012 20:47:13 +0100 |
wenzelm |
init options on startup as well;
|
changeset |
files
|
| Mon, 19 Nov 2012 20:23:47 +0100 |
wenzelm |
theorem status about oracles/futures is no longer printed by default;
|
changeset |
files
|
| Mon, 19 Nov 2012 18:01:48 +0100 |
hoelzl |
tuned: use induction rule sigma_sets_induct_disjoint
|
changeset |
files
|
| Mon, 19 Nov 2012 16:09:11 +0100 |
hoelzl |
tuned FinMap
|
changeset |
files
|
| Mon, 19 Nov 2012 12:29:02 +0100 |
hoelzl |
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
|
changeset |
files
|
| Mon, 19 Nov 2012 16:14:18 +0100 |
wenzelm |
more refs;
|
changeset |
files
|
| Sun, 18 Nov 2012 19:01:30 +0100 |
wenzelm |
isabelle build no longer supports document_dump/document_dump_mode (no INCOMPATIBILITY, since it was never in official release);
|
changeset |
files
|
| Sun, 18 Nov 2012 16:31:41 +0100 |
wenzelm |
proper jvmpath for windows;
|
changeset |
files
|
| Sun, 18 Nov 2012 16:04:13 +0100 |
wenzelm |
more generous tracing_limit, with explicit system option;
|
changeset |
files
|
| Sun, 18 Nov 2012 15:38:37 +0100 |
wenzelm |
adjust max_threads_value to capabilities of Poly/ML 5.5 and current hardware;
|
changeset |
files
|
| Sun, 18 Nov 2012 15:28:58 +0100 |
wenzelm |
update options via protocol;
|
changeset |
files
|
| Sun, 18 Nov 2012 14:24:30 +0100 |
wenzelm |
more accurate pixel_range -- do not round offset here;
|
changeset |
files
|
| Sun, 18 Nov 2012 13:52:54 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Sat, 17 Nov 2012 21:01:11 +0100 |
wenzelm |
prefer absolute default $USER_HOME/Scratch.thy;
|
changeset |
files
|
| Sat, 17 Nov 2012 20:47:56 +0100 |
wenzelm |
more portable process exit;
|
changeset |
files
|
| Sat, 17 Nov 2012 20:38:57 +0100 |
wenzelm |
tuned -- eliminate pointless ML method definition;
|
changeset |
files
|
| Sat, 17 Nov 2012 20:29:17 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 17 Nov 2012 20:19:34 +0100 |
wenzelm |
NEWS;
|
changeset |
files
|
| Sat, 17 Nov 2012 20:10:28 +0100 |
wenzelm |
tuned structure of Isabelle/HOL;
|
changeset |
files
|
| Sat, 17 Nov 2012 19:46:32 +0100 |
wenzelm |
method setup for Classical steps;
|
changeset |
files
|
| Sat, 17 Nov 2012 17:55:52 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Sat, 17 Nov 2012 17:42:19 +0100 |
wenzelm |
updated keywords;
|
changeset |
files
|
| Fri, 16 Nov 2012 19:14:23 +0100 |
hoelzl |
moved (b)choice_iff(') to Hilbert_Choice
|
changeset |
files
|
| Fri, 16 Nov 2012 18:45:57 +0100 |
hoelzl |
move theorems to be more generally useable
|
changeset |
files
|
| Fri, 16 Nov 2012 18:49:46 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 16 Nov 2012 16:59:56 +0100 |
wenzelm |
made SML/NJ happy;
|
changeset |
files
|
| Fri, 16 Nov 2012 14:46:23 +0100 |
hoelzl |
renamed prob_space to proj_prob_space as it clashed with Probability_Measure.prob_space
|
changeset |
files
|
| Fri, 16 Nov 2012 14:46:23 +0100 |
hoelzl |
renamed measurable_compose -> measurable_finmap_compose, clashed with Sigma_Algebra.measurable_compose
|
changeset |
files
|
| Fri, 16 Nov 2012 14:46:23 +0100 |
hoelzl |
measurability for nat_case and comb_seq
|
changeset |
files
|
| Fri, 16 Nov 2012 14:46:23 +0100 |
hoelzl |
rules for AE and prob
|
changeset |
files
|
| Fri, 16 Nov 2012 14:46:23 +0100 |
hoelzl |
rules for intergration: integrating nat-functions, integrals on finite measures, constant multiplication
|
changeset |
files
|
| Fri, 16 Nov 2012 12:10:02 +0100 |
hoelzl |
more measurability rules
|
changeset |
files
|
| Fri, 16 Nov 2012 11:34:34 +0100 |
immler |
renamed to more appropriate lim_P for projective limit
|
changeset |
files
|
| Fri, 16 Nov 2012 11:22:22 +0100 |
immler |
allow arbitrary enumerations of basis in locale for generation of borel sets
|
changeset |
files
|
| Thu, 15 Nov 2012 17:40:46 +0100 |
haftmann |
repaired slip accidentally introduced in 57209cfbf16b
|
changeset |
files
|
| Thu, 15 Nov 2012 12:11:15 +0100 |
haftmann |
prefer implementation in HOL;
|
changeset |
files
|
| Thu, 15 Nov 2012 17:36:08 +0100 |
immler |
corrected headers
|
changeset |
files
|
| Thu, 15 Nov 2012 16:07:52 +0100 |
immler |
hide constants of auxiliary type finmap
|
changeset |
files
|
| Thu, 15 Nov 2012 15:50:01 +0100 |
immler |
generalized to copy of countable types instead of instantiation of nat for discrete topology
|
changeset |
files
|
| Thu, 15 Nov 2012 11:16:58 +0100 |
immler |
added projective limit;
|
changeset |
files
|
| Thu, 15 Nov 2012 10:49:58 +0100 |
immler |
regularity of measures, therefore:
|
changeset |
files
|
| Thu, 15 Nov 2012 14:04:23 +0100 |
wenzelm |
tuned -- eliminated obsolete citation of isabelle-ref;
|
changeset |
files
|
| Mon, 12 Nov 2012 22:09:52 +0100 |
wenzelm |
updated basic equality rules;
|
changeset |
files
|
| Mon, 12 Nov 2012 21:17:58 +0100 |
wenzelm |
removed somewhat pointless historic material;
|
changeset |
files
|
| Sun, 11 Nov 2012 21:08:11 +0100 |
wenzelm |
updated unification options;
|
changeset |
files
|
| Sun, 11 Nov 2012 20:47:04 +0100 |
wenzelm |
removed some historic material that is obsolete or rarely used;
|
changeset |
files
|
| Sun, 11 Nov 2012 20:31:46 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 11 Nov 2012 16:19:55 +0100 |
wenzelm |
updated section on ordered rewriting;
|
changeset |
files
|
| Sat, 10 Nov 2012 20:16:16 +0100 |
wenzelm |
updated subgoaler/solver/looper;
|
changeset |
files
|
| Thu, 08 Nov 2012 20:25:48 +0100 |
wenzelm |
removed somewhat pointless historic material;
|
changeset |
files
|
| Thu, 08 Nov 2012 20:20:38 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 08 Nov 2012 20:18:34 +0100 |
wenzelm |
updated explanation of rewrite rules;
|
changeset |
files
|
| Wed, 07 Nov 2012 21:43:02 +0100 |
wenzelm |
(re)moved old material about Simplifier;
|
changeset |
files
|
| Wed, 07 Nov 2012 16:45:33 +0100 |
wenzelm |
some coverage of "resolution without lifting", which should be normally avoided;
|
changeset |
files
|
| Wed, 07 Nov 2012 16:09:39 +0100 |
wenzelm |
removed somewhat pointless historic material;
|
changeset |
files
|
| Wed, 07 Nov 2012 16:02:43 +0100 |
wenzelm |
updated biresolve_tac, bimatch_tac;
|
changeset |
files
|
| Wed, 07 Nov 2012 12:14:38 +0100 |
wenzelm |
moved classical wrappers to IsarRef;
|
changeset |
files
|
| Sun, 04 Nov 2012 20:23:26 +0100 |
wenzelm |
avoid clash of terminology wrt. "semi-automated" in the sense of Isar (e.g. method "rule");
|
changeset |
files
|
| Sun, 04 Nov 2012 20:12:01 +0100 |
wenzelm |
updated citations;
|
changeset |
files
|
| Sun, 04 Nov 2012 20:11:19 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 04 Nov 2012 20:11:05 +0100 |
wenzelm |
removed junk;
|
changeset |
files
|
| Sun, 04 Nov 2012 20:01:26 +0100 |
wenzelm |
removed pointless historic material;
|
changeset |
files
|
| Sun, 04 Nov 2012 19:51:53 +0100 |
wenzelm |
more on Simplifier rules, based on old material;
|
changeset |
files
|
| Sun, 04 Nov 2012 19:05:34 +0100 |
wenzelm |
refurbished Simplifier examples;
|
changeset |
files
|
| Sat, 03 Nov 2012 21:31:40 +0100 |
wenzelm |
more on the Simplifier, based on old material;
|
changeset |
files
|
| Sat, 03 Nov 2012 19:07:07 +0100 |
wenzelm |
more concise/precise documentation;
|
changeset |
files
|
| Wed, 14 Nov 2012 14:45:14 +0100 |
nipkow |
tuned text
|
changeset |
files
|
| Wed, 14 Nov 2012 14:11:47 +0100 |
nipkow |
replaced relation by function - simplifies development
|
changeset |
files
|
| Tue, 13 Nov 2012 12:12:14 +0100 |
traytel |
made SMLNJ happier
|
changeset |
files
|
| Tue, 13 Nov 2012 12:06:43 +0100 |
traytel |
import Sublist rather than PrefixOrder to avoid unnecessary class instantiation
|
changeset |
files
|
| Tue, 13 Nov 2012 09:08:32 +0100 |
haftmann |
prefer explicit Random.seed
|
changeset |
files
|
| Mon, 12 Nov 2012 23:24:40 +0100 |
haftmann |
dropped dead code
|
changeset |
files
|
| Mon, 12 Nov 2012 23:24:40 +0100 |
haftmann |
tuned import order
|
changeset |
files
|
| Mon, 12 Nov 2012 18:42:49 +0100 |
nipkow |
tuned layout
|
changeset |
files
|
| Mon, 12 Nov 2012 14:46:42 +0100 |
blanchet |
fixed detection of tautologies -- things like "a = b" in a structured proof, where a and b are Frees, shouldn't be discarted as tautologies
|
changeset |
files
|
| Mon, 12 Nov 2012 14:11:51 +0100 |
blanchet |
create temp directory if not already created
|
changeset |
files
|
| Mon, 12 Nov 2012 12:28:19 +0100 |
nipkow |
merged
|
changeset |
files
|
| Mon, 12 Nov 2012 12:27:58 +0100 |
nipkow |
new theory IMP/Finite_Reachable
|
changeset |
files
|
| Mon, 12 Nov 2012 12:06:56 +0100 |
blanchet |
avoid messing too much with output of "string_of_term", so that it doesn't break the yxml encoding for jEdit
|
changeset |
files
|
| Mon, 12 Nov 2012 11:52:37 +0100 |
blanchet |
centralized term printing code
|
changeset |
files
|
| Mon, 12 Nov 2012 11:32:22 +0100 |
blanchet |
thread context correctly when printing backquoted facts
|
changeset |
files
|
| Sun, 11 Nov 2012 19:56:02 +0100 |
haftmann |
dropped dead code;
|
changeset |
files
|
| Sun, 11 Nov 2012 19:24:01 +0100 |
haftmann |
modernized, simplified and compacted oracle and proof method glue code;
|
changeset |
files
|
| Fri, 09 Nov 2012 19:21:47 +0100 |
nipkow |
merged
|
changeset |
files
|
| Fri, 09 Nov 2012 19:16:31 +0100 |
nipkow |
fixed underscores
|
changeset |
files
|
| Fri, 09 Nov 2012 14:31:26 +0100 |
immler |
moved lemmas into projective_family; added header for theory Projective_Family
|
changeset |
files
|
| Fri, 09 Nov 2012 14:14:45 +0100 |
immler |
removed redundant/unnecessary assumptions from projective_family
|
changeset |
files
|
| Wed, 07 Nov 2012 14:41:49 +0100 |
immler |
assume probability spaces; allow empty index set
|
changeset |
files
|
| Wed, 07 Nov 2012 11:33:27 +0100 |
immler |
added projective_family; generalized generator in product_prob_space to projective_family
|
changeset |
files
|
| Tue, 06 Nov 2012 11:03:28 +0100 |
immler |
moved lemmas further up
|
changeset |
files
|
| Thu, 08 Nov 2012 20:02:41 +0100 |
bulwahn |
tuned proofs
|
changeset |
files
|
| Thu, 08 Nov 2012 19:55:37 +0100 |
bulwahn |
using hyp_subst_tac that allows to pass the current simpset to avoid the renamed bound variable warning in the simplifier
|
changeset |
files
|
| Thu, 08 Nov 2012 19:55:35 +0100 |
bulwahn |
hyp_subst_tac allows to pass an optional simpset to the internal simplifier call to avoid renamed bound variable warnings in the simplifier call
|
changeset |
files
|
| Thu, 08 Nov 2012 19:55:19 +0100 |
bulwahn |
NEWS
|
changeset |
files
|
| Thu, 08 Nov 2012 19:55:17 +0100 |
bulwahn |
rewriting with the simpset that is passed to the simproc
|
changeset |
files
|
| Thu, 08 Nov 2012 17:11:04 +0100 |
bulwahn |
handling x : S y pattern with the default mechanism instead of raising an exception in the set_comprehension_pointfree simproc
|
changeset |
files
|
| Thu, 08 Nov 2012 17:06:59 +0100 |
bulwahn |
tuned
|
changeset |
files
|
| Thu, 08 Nov 2012 16:25:26 +0100 |
bulwahn |
syntactic tuning and restructuring of set_comprehension_pointfree simproc
|
changeset |
files
|
| Thu, 08 Nov 2012 11:59:50 +0100 |
bulwahn |
using more proper simpset in tactic of set_comprehension_pointfree simproc to avoid renamed bound variable warnings in recursive simplifier calls
|
changeset |
files
|
| Thu, 08 Nov 2012 11:59:49 +0100 |
bulwahn |
improving the extension of sets in case of more than one bound variable; rearranging the tactic to prefer simpler steps before more involved ones
|
changeset |
files
|
| Thu, 08 Nov 2012 11:59:48 +0100 |
bulwahn |
adjusting proofs as the set_comprehension_pointfree simproc breaks some existing proofs
|
changeset |
files
|
| Thu, 08 Nov 2012 11:59:47 +0100 |
bulwahn |
importing term with schematic type variables properly before passing it to the tactic in the set_comprehension_pointfree simproc
|
changeset |
files
|
| Thu, 08 Nov 2012 11:59:47 +0100 |
bulwahn |
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
|
changeset |
files
|
| Thu, 08 Nov 2012 11:59:46 +0100 |
bulwahn |
simplified structure of patterns in set_comprehension_simproc
|
changeset |
files
|
| Thu, 08 Nov 2012 10:02:38 +0100 |
haftmann |
refined stack of library theories implementing int and/or nat by target language numerals
|
changeset |
files
|
| Wed, 07 Nov 2012 20:48:04 +0100 |
haftmann |
restored SML code check which got unintentionally broken: must explicitly check for error during compilation;
|
changeset |
files
|
| Tue, 06 Nov 2012 19:18:35 +0100 |
hoelzl |
add support for function application to measurability prover
|
changeset |
files
|
| Tue, 06 Nov 2012 15:15:33 +0100 |
blanchet |
renamed Sledgehammer option
|
changeset |
files
|
| Tue, 06 Nov 2012 15:12:31 +0100 |
blanchet |
always show timing for structured proofs
|
changeset |
files
|
| Tue, 06 Nov 2012 14:46:21 +0100 |
blanchet |
use implications rather than disjunctions to improve readability
|
changeset |
files
|
| Tue, 06 Nov 2012 13:47:51 +0100 |
blanchet |
avoid name clashes
|
changeset |
files
|
| Tue, 06 Nov 2012 13:09:02 +0100 |
blanchet |
fixed more "Trueprop" issues
|
changeset |
files
|
| Tue, 06 Nov 2012 12:38:45 +0100 |
blanchet |
removed needless sort
|
changeset |
files
|
| Tue, 06 Nov 2012 11:24:48 +0100 |
blanchet |
avoid double "Trueprop"s
|
changeset |
files
|
| Tue, 06 Nov 2012 11:20:56 +0100 |
blanchet |
use original formulas for hypotheses and conclusion to avoid mismatches
|
changeset |
files
|
| Tue, 06 Nov 2012 11:20:56 +0100 |
blanchet |
track formula roles in proofs and use that to determine whether the conjecture should be negated or not
|
changeset |
files
|
| Tue, 06 Nov 2012 11:20:56 +0100 |
blanchet |
correct parsing of E dependencies
|
changeset |
files
|
| Tue, 06 Nov 2012 11:20:56 +0100 |
blanchet |
proper handling of assumptions arising from the goal's being expressed in rule format, for Isar proof construction
|
changeset |
files
|
| Mon, 05 Nov 2012 11:40:51 +0100 |
nipkow |
tuned
|
changeset |
files
|
| Sun, 04 Nov 2012 18:41:27 +0100 |
nipkow |
code for while directly, not via while_option
|
changeset |
files
|
| Sun, 04 Nov 2012 18:38:18 +0100 |
nipkow |
executable true liveness analysis incl an approximating version
|
changeset |
files
|
| Sun, 04 Nov 2012 17:36:26 +0100 |
nipkow |
now that sets are executable again, no more special treatment of variable sets
|
changeset |
files
|
| Fri, 02 Nov 2012 16:16:48 +0100 |
blanchet |
handle non-unit clauses gracefully
|
changeset |
files
|
| Fri, 02 Nov 2012 16:16:48 +0100 |
blanchet |
several improvements to Isar proof reconstruction, by Steffen Smolka (step merging in case splits, time measurements, etc.)
|
changeset |
files
|
| Fri, 02 Nov 2012 14:23:54 +0100 |
hoelzl |
use measurability prover
|
changeset |
files
|
| Fri, 02 Nov 2012 14:23:40 +0100 |
hoelzl |
add measurability prover; add support for Borel sets
|
changeset |
files
|
| Fri, 02 Nov 2012 14:00:39 +0100 |
hoelzl |
add syntax and a.e.-rules for (conditional) probability on predicates
|
changeset |
files
|
| Fri, 02 Nov 2012 14:00:39 +0100 |
hoelzl |
infinite product measure is invariant under adding prefixes
|
changeset |
files
|
| Fri, 02 Nov 2012 14:00:39 +0100 |
hoelzl |
for the product measure it is enough if only one measure is sigma-finite
|
changeset |
files
|
| Fri, 02 Nov 2012 12:00:51 +0100 |
berghofe |
Allow parentheses around left-hand sides of array associations
|
changeset |
files
|
| Thu, 01 Nov 2012 15:00:48 +0100 |
blanchet |
made MaSh more robust in the face of duplicate "nicknames" (which can happen e.g. if you have a lemma called foo(1) and another called foo_1 in the same theory)
|
changeset |
files
|
| Thu, 01 Nov 2012 13:32:57 +0100 |
blanchet |
regenerated SMT certificates
|
changeset |
files
|
| Thu, 01 Nov 2012 11:34:00 +0100 |
blanchet |
regenerated "SMT_Examples" certificates after soft-timeout change + removed a few needless oracles
|
changeset |
files
|
| Wed, 31 Oct 2012 11:23:21 +0100 |
blanchet |
fixed bool vs. prop mismatch
|
changeset |
files
|
| Wed, 31 Oct 2012 11:23:21 +0100 |
blanchet |
removed "refute" command from Isar manual, now that it has been moved outside "Main"
|
changeset |
files
|
| Wed, 31 Oct 2012 11:23:21 +0100 |
blanchet |
repaired "Mutabelle" after Refute move
|
changeset |
files
|
| Wed, 31 Oct 2012 11:23:21 +0100 |
blanchet |
less verbose -- the warning will reach the users anyway by other means
|
changeset |
files
|
| Wed, 31 Oct 2012 11:23:21 +0100 |
blanchet |
tuned messages
|
changeset |
files
|
| Wed, 31 Oct 2012 11:23:21 +0100 |
blanchet |
moved "SAT" before "FunDef" and moved back all SAT-related ML files to where they belong
|
changeset |
files
|
| Wed, 31 Oct 2012 11:23:21 +0100 |
blanchet |
fixes related to Refute's move
|
changeset |
files
|
| Wed, 31 Oct 2012 11:23:21 +0100 |
blanchet |
added a timeout around script that relies on the network
|
changeset |
files
|
| Wed, 31 Oct 2012 11:23:21 +0100 |
blanchet |
took out "using only ..." comments in Sledgehammer generated metis/smt calls, until these can be generated soundly
|
changeset |
files
|
| Wed, 31 Oct 2012 11:23:21 +0100 |
blanchet |
moved Refute to "HOL/Library" to speed up building "Main" even more
|
changeset |
files
|
| Wed, 31 Oct 2012 11:23:21 +0100 |
blanchet |
tuning
|
changeset |
files
|
| Wed, 31 Oct 2012 11:23:21 +0100 |
blanchet |
use metaquantification when possible in Isar proofs
|
changeset |
files
|
| Wed, 31 Oct 2012 11:23:21 +0100 |
blanchet |
tuned code
|
changeset |
files
|
| Wed, 31 Oct 2012 11:23:21 +0100 |
blanchet |
tuning
|
changeset |
files
|
| Wed, 31 Oct 2012 11:23:21 +0100 |
blanchet |
soft SMT timeout
|
changeset |
files
|
| Sun, 28 Oct 2012 02:22:39 +0000 |
Christian Urban |
added function store_termination_rule to the signature, as it is used in Nominal2
|
changeset |
files
|
| Sat, 27 Oct 2012 20:59:50 +0200 |
wenzelm |
longer log, to accomodate final status line of isabelle build;
|
changeset |
files
|
| Wed, 24 Oct 2012 18:43:25 +0200 |
huffman |
transfer package: error message if preprocessing goal to object-logic formula fails
|
changeset |
files
|
| Wed, 24 Oct 2012 18:43:25 +0200 |
huffman |
transfer package: add test to prevent trying to make cterms from open terms
|
changeset |
files
|
| Wed, 24 Oct 2012 18:43:25 +0200 |
huffman |
transfer package: more flexible handling of equality relations using is_equality predicate
|
changeset |
files
|
| Wed, 24 Oct 2012 17:40:56 +0200 |
nipkow |
ensured that rewr_conv rule t = "t == u" literally not just modulo beta-eta
|
changeset |
files
|
| Mon, 22 Oct 2012 22:47:14 +0200 |
kuncar |
new theorems
|
changeset |
files
|
| Mon, 22 Oct 2012 22:24:34 +0200 |
haftmann |
incorporated constant chars into instantiation proof for enum;
|
changeset |
files
|
| Mon, 22 Oct 2012 19:02:36 +0200 |
haftmann |
close code theorems explicitly after preprocessing
|
changeset |
files
|
| Mon, 22 Oct 2012 17:09:49 +0200 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Mon, 22 Oct 2012 16:27:55 +0200 |
wenzelm |
further attempts to cope with large files via option jedit_text_overview_limit;
|
changeset |
files
|
| Mon, 22 Oct 2012 14:52:38 +0200 |
wenzelm |
more detailed Prover IDE NEWS;
|
changeset |
files
|
| Sun, 21 Oct 2012 22:32:22 +0200 |
wenzelm |
recovered explicit error message, which was lost in b8570ea1ce25;
|
changeset |
files
|
| Sun, 21 Oct 2012 22:31:39 +0200 |
wenzelm |
removed dead code;
|
changeset |
files
|
| Sun, 21 Oct 2012 22:12:22 +0200 |
wenzelm |
proper signatures;
|
changeset |
files
|
| Sun, 21 Oct 2012 22:11:38 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 21 Oct 2012 17:04:13 +0200 |
webertj |
merged
|
changeset |
files
|
| Fri, 19 Oct 2012 15:12:52 +0200 |
webertj |
Renamed {left,right}_distrib to distrib_{right,left}.
|
changeset |
files
|
| Fri, 19 Oct 2012 10:46:42 +0200 |
webertj |
Tuned.
|
changeset |
files
|
| Sun, 21 Oct 2012 16:43:08 +0200 |
haftmann |
more conventional argument order;
|
changeset |
files
|
| Sun, 21 Oct 2012 08:39:41 +0200 |
bulwahn |
another refinement in the comprehension conversion
|
changeset |
files
|
| Sun, 21 Oct 2012 05:24:59 +0200 |
bulwahn |
refined simplifier call in comprehension_conv
|
changeset |
files
|
| Sun, 21 Oct 2012 05:24:56 +0200 |
bulwahn |
passing around the simpset instead of the context; rewriting tactics to avoid the 'renamed bound variable' warnings in nested simplifier calls
|
changeset |
files
|
| Sat, 20 Oct 2012 17:40:51 +0200 |
wenzelm |
avoid STIX font, which tends to render badly;
|
changeset |
files
|
| Sat, 20 Oct 2012 17:15:40 +0200 |
wenzelm |
extra jar for scala-2.10.0-RC1;
|
changeset |
files
|
| Sat, 20 Oct 2012 15:46:48 +0200 |
wenzelm |
more explicit auxiliary classes to avoid warning "reflective access of structural type member method" of scala-2.10.0-RC1;
|
changeset |
files
|
| Sat, 20 Oct 2012 15:45:40 +0200 |
wenzelm |
avoid duplicate build of jars_fresh;
|
changeset |
files
|
| Sat, 20 Oct 2012 12:01:20 +0200 |
wenzelm |
obsolete, cf. README_REPOSITORY;
|
changeset |
files
|
| Sat, 20 Oct 2012 12:00:48 +0200 |
wenzelm |
accomodate scala-2.10.0-RC1;
|
changeset |
files
|
| Sat, 20 Oct 2012 10:00:21 +0200 |
haftmann |
tailored enum specification towards simple instantiation;
|
changeset |
files
|
| Sat, 20 Oct 2012 10:00:21 +0200 |
haftmann |
refined internal structure of Enum.thy
|
changeset |
files
|
| Sat, 20 Oct 2012 09:12:16 +0200 |
haftmann |
moved quite generic material from theory Enum to more appropriate places
|
changeset |
files
|
| Sat, 20 Oct 2012 09:09:37 +0200 |
bulwahn |
adding another test case for the set_comprehension_simproc to the theory in HOL/ex
|
changeset |
files
|
| Sat, 20 Oct 2012 09:09:35 +0200 |
bulwahn |
improving tactic in setcomprehension_simproc
|
changeset |
files
|
| Sat, 20 Oct 2012 09:09:34 +0200 |
bulwahn |
adjusting proofs
|
changeset |
files
|
| Sat, 20 Oct 2012 09:09:33 +0200 |
bulwahn |
tuned tactic in set_comprehension_pointfree simproc to handle composition of negation and vimage
|
changeset |
files
|
| Sat, 20 Oct 2012 09:09:32 +0200 |
bulwahn |
passing names and types of all bounds around in the simproc
|
changeset |
files
|
| Thu, 18 Oct 2012 10:06:27 +0200 |
bulwahn |
locally inverting previously applied simplifications with ex_simps in set_comprehension_pointfree
|
changeset |
files
|
| Fri, 19 Oct 2012 21:52:45 +0200 |
wenzelm |
more precise pixel_range: avoid popup when pointing into empty space after actual end-of-line;
|
changeset |
files
|
| Fri, 19 Oct 2012 21:19:06 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 19 Oct 2012 17:54:16 +0200 |
kuncar |
don't include Quotient_Option - workaround to a transfer bug
|
changeset |
files
|
| Fri, 19 Oct 2012 21:18:34 +0200 |
wenzelm |
ignore old stuff and thus speed up the script greatly;
|
changeset |
files
|
| Fri, 19 Oct 2012 20:15:14 +0200 |
wenzelm |
proper find -mtime (file data) instead of -ctime (meta data);
|
changeset |
files
|
| Fri, 19 Oct 2012 17:52:21 +0200 |
wenzelm |
made SML/NJ happy;
|
changeset |
files
|
| Fri, 19 Oct 2012 12:08:13 +0200 |
wenzelm |
clarified Future.map (again): finished value is mapped in-place, which saves task structures and changes error behaviour slightly (tolerance against canceled group of old value etc.);
|
changeset |
files
|
| Thu, 18 Oct 2012 20:59:46 +0200 |
wenzelm |
back to polyml-5.4.1 (cf. b3110dec1a32) -- no cause of spurious interrupts;
|
changeset |
files
|
| Thu, 18 Oct 2012 20:45:15 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 18 Oct 2012 20:00:45 +0200 |
wenzelm |
back to parallel HOL-BNF-Examples, which seems to have suffered from Future.map on canceled persistent futures;
|
changeset |
files
|
| Thu, 18 Oct 2012 19:58:30 +0200 |
wenzelm |
more basic Goal.reset_futures as snapshot of implicit state;
|
changeset |
files
|
| Thu, 18 Oct 2012 19:12:58 +0200 |
wenzelm |
tuned proof;
|
changeset |
files
|
| Thu, 18 Oct 2012 15:52:33 +0200 |
kuncar |
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
|
changeset |
files
|
| Thu, 18 Oct 2012 15:52:32 +0200 |
kuncar |
tuned proofs
|
changeset |
files
|
| Thu, 18 Oct 2012 15:52:31 +0200 |
kuncar |
new theorem
|
changeset |
files
|
| Thu, 18 Oct 2012 15:47:01 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 18 Oct 2012 15:44:14 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 18 Oct 2012 15:28:49 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 18 Oct 2012 15:16:39 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 18 Oct 2012 15:15:08 +0200 |
wenzelm |
fixed proof (cf. a81f95693c68);
|
changeset |
files
|
| Thu, 18 Oct 2012 15:41:15 +0200 |
blanchet |
tuned Isar output
|
changeset |
files
|
| Thu, 18 Oct 2012 15:40:02 +0200 |
nipkow |
tuned
|
changeset |
files
|
| Thu, 18 Oct 2012 15:10:49 +0200 |
blanchet |
updated docs
|
changeset |
files
|
| Thu, 18 Oct 2012 15:05:17 +0200 |
blanchet |
renamed Isar-proof related options + changed semantics of Isar shrinking
|
changeset |
files
|
| Thu, 18 Oct 2012 14:26:45 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Thu, 18 Oct 2012 13:46:24 +0200 |
blanchet |
fixed theorem lookup code in Isar proof reconstruction
|
changeset |
files
|
| Thu, 18 Oct 2012 13:37:53 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Thu, 18 Oct 2012 13:19:44 +0200 |
blanchet |
refactor code
|
changeset |
files
|
| Thu, 18 Oct 2012 11:59:45 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Thu, 18 Oct 2012 14:15:46 +0200 |
wenzelm |
more robust future_proof result with specific error message (e.g. relevant for incomplete proof of non-registered theorem);
|
changeset |
files
|
| Thu, 18 Oct 2012 13:57:27 +0200 |
wenzelm |
collective errors from use_thys and Session.finish/Goal.finish_futures -- avoid uninformative interrupts stemming from failure of goal forks that are not registered in the theory (e.g. unnamed theorems);
|
changeset |
files
|
| Thu, 18 Oct 2012 13:53:02 +0200 |
wenzelm |
more uniform group for map_future, which is relevant for cancel in worker_task vs. future_job -- prefer peer group despite 81d03a29980c;
|
changeset |
files
|
| Thu, 18 Oct 2012 13:26:49 +0200 |
wenzelm |
tuned message;
|
changeset |
files
|
| Thu, 18 Oct 2012 12:47:30 +0200 |
wenzelm |
tuned comment;
|
changeset |
files
|
| Thu, 18 Oct 2012 12:26:30 +0200 |
wenzelm |
avoid spurious "bad" markup for show/test_proof;
|
changeset |
files
|
| Thu, 18 Oct 2012 12:00:27 +0200 |
wenzelm |
more official Future.terminate;
|
changeset |
files
|
| Thu, 18 Oct 2012 09:19:37 +0200 |
haftmann |
simp results for simplification results of Inf/Sup expressions on bool;
|
changeset |
files
|
| Thu, 18 Oct 2012 09:17:00 +0200 |
haftmann |
no sort constraints on datatype constructors in internal bookkeeping
|
changeset |
files
|
| Wed, 17 Oct 2012 22:57:28 +0200 |
wenzelm |
HOL-BNF-Examples is sequential for now, due to spurious interrupts (again);
|
changeset |
files
|
| Wed, 17 Oct 2012 22:45:40 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 17 Oct 2012 15:25:52 +0200 |
bulwahn |
comprehension conversion reuses suggested names for bound variables instead of invented fresh ones; tuned tactic
|
changeset |
files
|
| Wed, 17 Oct 2012 14:13:57 +0200 |
bulwahn |
checking for bound variables in the set expression; handling negation more generally
|
changeset |
files
|
| Wed, 17 Oct 2012 14:13:57 +0200 |
bulwahn |
set_comprehension_pointfree simproc now handles the complicated test case; tuned
|
changeset |
files
|
| Wed, 17 Oct 2012 14:13:57 +0200 |
bulwahn |
refined conversion to only react on proper set comprehensions; tuned
|
changeset |
files
|
| Wed, 17 Oct 2012 14:13:57 +0200 |
bulwahn |
moving Pair_inject from legacy and duplicate section to general section, as Pair_inject was considered a duplicate in e8400e31528a by mistake (cf. communication on dev mailing list)
|
changeset |
files
|
| Wed, 17 Oct 2012 14:13:57 +0200 |
bulwahn |
employing a preprocessing conversion that rewrites {(x1, ..., xn). P x1 ... xn} to {(x1, ..., xn) | x1 ... xn. P x1 ... xn} in set_comprehension_pointfree simproc
|
changeset |
files
|
| Wed, 17 Oct 2012 22:11:12 +0200 |
wenzelm |
another Future.shutdown after Future.cancel_groups (cf. 0d4106850eb2);
|
changeset |
files
|
| Wed, 17 Oct 2012 21:18:32 +0200 |
wenzelm |
more robust cancel_now: avoid shooting yourself in the foot;
|
changeset |
files
|
| Wed, 17 Oct 2012 21:04:51 +0200 |
wenzelm |
more robust Session.finish (batch mode): use Goal.finish_futures to exhibit remaining failures of disconnected goal forks (e.g. from unnamed theorems) and Goal.cancel_futures the purge the persistent state;
|
changeset |
files
|
| Wed, 17 Oct 2012 14:58:04 +0200 |
wenzelm |
proper 'oops' to force sequential checking here, and avoid spurious *** Interrupt stemming from crash of forked outer syntax element;
|
changeset |
files
|
| Wed, 17 Oct 2012 14:39:00 +0200 |
wenzelm |
added Output "Detach" button;
|
changeset |
files
|
| Wed, 17 Oct 2012 14:20:54 +0200 |
wenzelm |
skipped proofs appear as "bad" without counting as error;
|
changeset |
files
|
| Wed, 17 Oct 2012 13:20:08 +0200 |
wenzelm |
more method position information, notably finished_pos after end of previous text;
|
changeset |
files
|
| Wed, 17 Oct 2012 10:46:14 +0200 |
wenzelm |
more formal markup;
|
changeset |
files
|
| Wed, 17 Oct 2012 10:45:43 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Wed, 17 Oct 2012 10:26:27 +0200 |
wenzelm |
more formal markup;
|
changeset |
files
|
| Wed, 17 Oct 2012 00:16:31 +0200 |
kuncar |
don't be so aggressive when expanding a transfer rule relation; rewrite only the relational part of the rule
|
changeset |
files
|
| Tue, 16 Oct 2012 22:38:34 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 16 Oct 2012 20:31:08 +0200 |
blanchet |
added missing file
|
changeset |
files
|
| Tue, 16 Oct 2012 20:11:15 +0200 |
traytel |
tuned for document output
|
changeset |
files
|
| Tue, 16 Oct 2012 18:50:53 +0200 |
blanchet |
added proof minimization code from Steffen Smolka
|
changeset |
files
|
| Tue, 16 Oct 2012 18:07:59 +0200 |
traytel |
tuned blank lines
|
changeset |
files
|
| Tue, 16 Oct 2012 18:05:28 +0200 |
traytel |
tuned whitespace
|
changeset |
files
|
| Tue, 16 Oct 2012 17:33:08 +0200 |
popescua |
a few notations changed in HOL/BNF/Examples/Derivation_Trees
|
changeset |
files
|
| Tue, 16 Oct 2012 17:08:20 +0200 |
popescua |
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
|
changeset |
files
|
| Tue, 16 Oct 2012 13:57:08 +0200 |
bulwahn |
adding test cases for f x y : S patterns in set_comprehension_pointfree simproc
|
changeset |
files
|
| Tue, 16 Oct 2012 13:18:13 +0200 |
bulwahn |
tactic of set_comprehension_pointfree simproc handles f x y : S patterns with Set.vimage
|
changeset |
files
|
| Tue, 16 Oct 2012 13:18:12 +0200 |
bulwahn |
term construction of set_comprehension_pointfree simproc handles f x y : S patterns with Set.vimage
|
changeset |
files
|
| Tue, 16 Oct 2012 13:18:10 +0200 |
bulwahn |
extending preprocessing of simproc to rewrite subset inequality into membership of powerset
|
changeset |
files
|
| Tue, 16 Oct 2012 13:15:58 +0200 |
popescua |
update ROOT with teh directory change in BNF
|
changeset |
files
|
| Tue, 16 Oct 2012 13:09:46 +0200 |
popescua |
changed name of BNF/Example directory from Infinite_Derivation_Trees to Derivation_Trees
|
changeset |
files
|
| Tue, 16 Oct 2012 22:13:46 +0200 |
wenzelm |
retain info dockable state via educated guess on window focus;
|
changeset |
files
|
| Tue, 16 Oct 2012 21:30:52 +0200 |
wenzelm |
support for more informative errors in lazy enumerations;
|
changeset |
files
|
| Tue, 16 Oct 2012 21:26:36 +0200 |
wenzelm |
more informative errors for 'also' and 'finally';
|
changeset |
files
|
| Tue, 16 Oct 2012 20:35:24 +0200 |
wenzelm |
tuned messages;
|
changeset |
files
|
| Tue, 16 Oct 2012 20:23:00 +0200 |
wenzelm |
more proof method text position information;
|
changeset |
files
|
| Tue, 16 Oct 2012 17:47:23 +0200 |
wenzelm |
clarified defer/prefer: more specific errors;
|
changeset |
files
|
| Tue, 16 Oct 2012 16:50:03 +0200 |
wenzelm |
updated Toplevel.proofs;
|
changeset |
files
|
| Tue, 16 Oct 2012 15:14:12 +0200 |
wenzelm |
more informative errors for 'proof' and 'apply' steps;
|
changeset |
files
|
| Tue, 16 Oct 2012 15:02:49 +0200 |
wenzelm |
more friendly handling of Pure.thy bootstrap errors;
|
changeset |
files
|
| Tue, 16 Oct 2012 14:14:37 +0200 |
wenzelm |
more informative error for stand-alone 'qed';
|
changeset |
files
|
| Tue, 16 Oct 2012 14:02:02 +0200 |
wenzelm |
further attempts to unify/simplify goal output;
|
changeset |
files
|
| Tue, 16 Oct 2012 13:06:40 +0200 |
wenzelm |
more informative error messages of initial/terminal proof methods;
|
changeset |
files
|
| Mon, 15 Oct 2012 19:03:02 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 15 Oct 2012 16:18:48 +0200 |
bulwahn |
setcomprehension_pointfree simproc also works for set comprehension without an equation
|
changeset |
files
|
| Mon, 15 Oct 2012 15:43:12 +0200 |
wenzelm |
tuned message -- avoid extra blank lines;
|
changeset |
files
|
| Mon, 15 Oct 2012 15:28:56 +0200 |
wenzelm |
updated to polyml-5.5.0 which reduces chance of HOL-IMP failure (although it is hard to reproduce anyway);
|
changeset |
files
|
| Sun, 14 Oct 2012 21:02:14 +0200 |
Markus Kaiser |
store colors after build
|
changeset |
files
|
| Sun, 14 Oct 2012 19:16:39 +0200 |
bulwahn |
adding further test cases for the set_comprehension_pointfree simproc
|
changeset |
files
|
| Sun, 14 Oct 2012 19:16:35 +0200 |
bulwahn |
refined tactic in set_comprehension_pointfree simproc
|
changeset |
files
|
| Sun, 14 Oct 2012 19:16:33 +0200 |
bulwahn |
adding further test cases to check new functionality of the simproc; strengthened test cases to check the success of the simproc more faithfully
|
changeset |
files
|
| Sun, 14 Oct 2012 19:16:32 +0200 |
bulwahn |
adding postprocessing of computed pointfree expression in set_comprehension_pointfree simproc
|
changeset |
files
|
| Sun, 14 Oct 2012 19:16:32 +0200 |
bulwahn |
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
|
changeset |
files
|
| Sat, 13 Oct 2012 21:09:20 +0200 |
wenzelm |
more informative error of initial/terminal proof steps;
|
changeset |
files
|
| Sat, 13 Oct 2012 19:53:04 +0200 |
wenzelm |
some attempts to unify/simplify pretty_goal;
|
changeset |
files
|
| Sat, 13 Oct 2012 18:04:11 +0200 |
wenzelm |
refined Proof.the_finished_goal with more informative error;
|
changeset |
files
|
| Sat, 13 Oct 2012 16:19:16 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Sat, 13 Oct 2012 00:08:36 +0200 |
wenzelm |
improved adhoc height for small fonts;
|
changeset |
files
|
| Fri, 12 Oct 2012 23:38:48 +0200 |
wenzelm |
further refinement of jEdit line range, avoiding lack of final \n;
|
changeset |
files
|
| Fri, 12 Oct 2012 22:53:20 +0200 |
wenzelm |
more uniform tooltip color;
|
changeset |
files
|
| Fri, 12 Oct 2012 22:10:45 +0200 |
wenzelm |
more NEWS;
|
changeset |
files
|
| Fri, 12 Oct 2012 21:51:25 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 12 Oct 2012 15:52:55 +0200 |
traytel |
disambiguated grammar
|
changeset |
files
|
| Fri, 12 Oct 2012 15:52:45 +0200 |
traytel |
tuned proofs
|
changeset |
files
|
| Fri, 12 Oct 2012 14:57:56 +0200 |
nipkow |
tuned
|
changeset |
files
|
| Fri, 12 Oct 2012 21:39:58 +0200 |
wenzelm |
simplified 'typedef' specifications: discontinued implicit set definition and alternative name;
|
changeset |
files
|
| Fri, 12 Oct 2012 21:22:35 +0200 |
wenzelm |
discontinued typedef with alternative name;
|
changeset |
files
|
| Fri, 12 Oct 2012 18:58:20 +0200 |
wenzelm |
discontinued obsolete typedef (open) syntax;
|
changeset |
files
|
| Fri, 12 Oct 2012 15:08:29 +0200 |
wenzelm |
discontinued typedef with implicit set_def;
|
changeset |
files
|
| Fri, 12 Oct 2012 14:05:30 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 12 Oct 2012 12:21:01 +0200 |
bulwahn |
increading indexes to avoid clashes in the set_comprehension_pointfree simproc
|
changeset |
files
|
| Fri, 12 Oct 2012 13:55:13 +0200 |
wenzelm |
no special treatment of errors inside goal forks without transaction id, to avoid duplication in plain build with sequential log, for example;
|
changeset |
files
|
| Fri, 12 Oct 2012 13:46:41 +0200 |
wenzelm |
do not treat interrupt as error here, to avoid confusion in log etc.;
|
changeset |
files
|
| Fri, 12 Oct 2012 11:03:23 +0200 |
wenzelm |
more basic ML compiler messages -- avoid conflict of 638cefe3ee99 and cb7264721c91 concerning Protocol.message_positions;
|
changeset |
files
|
| Thu, 11 Oct 2012 23:10:49 +0200 |
wenzelm |
refined separator: FBreak needs to be free for proper breaking, extra space at end helps to work around last-line oddity in jEdit;
|
changeset |
files
|
| Thu, 11 Oct 2012 21:02:19 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 11 Oct 2012 14:38:58 +0200 |
hoelzl |
cleanup borel_measurable_positive_integral_(fst|snd)
|
changeset |
files
|
| Thu, 11 Oct 2012 11:56:43 +0200 |
haftmann |
msetprod based directly on Multiset.fold;
|
changeset |
files
|
| Thu, 11 Oct 2012 11:56:43 +0200 |
haftmann |
avoid global interpretation
|
changeset |
files
|
| Thu, 11 Oct 2012 11:56:42 +0200 |
haftmann |
simplified construction of fold combinator on multisets;
|
changeset |
files
|
| Thu, 11 Oct 2012 20:38:02 +0200 |
wenzelm |
clarified output token markup (see also bc22daeed49e);
|
changeset |
files
|
| Thu, 11 Oct 2012 19:25:36 +0200 |
wenzelm |
refined aprop_tr' -- retain entity information by using type slot as adhoc marker;
|
changeset |
files
|
| Thu, 11 Oct 2012 16:09:44 +0200 |
wenzelm |
refrain from quantifying outer fixes, to enable nesting of contexts like "context fixes x context assumes A x";
|
changeset |
files
|
| Thu, 11 Oct 2012 15:26:33 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 11 Oct 2012 15:06:27 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 11 Oct 2012 12:38:18 +0200 |
wenzelm |
more position information for hyperlink and placement of message;
|
changeset |
files
|
| Thu, 11 Oct 2012 12:37:38 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 11 Oct 2012 00:13:21 +0200 |
krauss |
mira: discontinued special settings for lxbroy10, which are probably made obsolete by newer polyml
|
changeset |
files
|
| Wed, 10 Oct 2012 22:53:48 +0200 |
krauss |
removed unused legacy material from mira.py
|
changeset |
files
|
| Wed, 10 Oct 2012 17:43:23 +0200 |
wenzelm |
eliminated some remaining uses of typedef with implicit set definition;
|
changeset |
files
|
| Wed, 10 Oct 2012 16:41:19 +0200 |
Andreas Lochbihler |
merged
|
changeset |
files
|
| Wed, 10 Oct 2012 16:18:27 +0200 |
Andreas Lochbihler |
fix code equation for RBT_Impl.fold
|
changeset |
files
|
| Wed, 10 Oct 2012 15:17:18 +0200 |
Andreas Lochbihler |
merged
|
changeset |
files
|
| Wed, 10 Oct 2012 15:16:44 +0200 |
Andreas Lochbihler |
tail-recursive implementation for length
|
changeset |
files
|
| Wed, 10 Oct 2012 15:05:07 +0200 |
Andreas Lochbihler |
correct definition for skip_black
|
changeset |
files
|
| Wed, 10 Oct 2012 16:19:52 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 10 Oct 2012 13:30:50 +0200 |
hoelzl |
merged
|
changeset |
files
|
| Wed, 10 Oct 2012 12:12:37 +0200 |
hoelzl |
infprod generator works also with empty index set
|
changeset |
files
|
| Wed, 10 Oct 2012 12:12:36 +0200 |
hoelzl |
add finite entropy
|
changeset |
files
|
| Wed, 10 Oct 2012 12:12:36 +0200 |
hoelzl |
continuous version of mutual_information_eq_entropy_conditional_entropy
|
changeset |
files
|
| Wed, 10 Oct 2012 12:12:35 +0200 |
hoelzl |
add induction for real Borel measurable functions
|
changeset |
files
|
| Wed, 10 Oct 2012 12:12:34 +0200 |
hoelzl |
induction prove for positive_integral_fst
|
changeset |
files
|
| Wed, 10 Oct 2012 12:12:34 +0200 |
hoelzl |
strong nonnegativ (instead of ae nn) for induction rule
|
changeset |
files
|
| Wed, 10 Oct 2012 12:12:33 +0200 |
hoelzl |
induction prove for positive_integral_density
|
changeset |
files
|
| Wed, 10 Oct 2012 12:12:32 +0200 |
hoelzl |
add induction rules for simple functions and for Borel measurable functions
|
changeset |
files
|
| Wed, 10 Oct 2012 12:12:32 +0200 |
hoelzl |
introduce induction rules for simple functions and for Borel measurable functions
|
changeset |
files
|
| Wed, 10 Oct 2012 12:12:31 +0200 |
hoelzl |
joint distribution of independent variables
|
changeset |
files
|
| Wed, 10 Oct 2012 12:12:30 +0200 |
hoelzl |
indep_vars does not need sigma-sets
|
changeset |
files
|
| Wed, 10 Oct 2012 12:12:29 +0200 |
hoelzl |
simplified definitions
|
changeset |
files
|
| Wed, 10 Oct 2012 12:12:29 +0200 |
hoelzl |
remove unnecessary assumption from conditional_entropy_eq
|
changeset |
files
|
| Wed, 10 Oct 2012 12:12:28 +0200 |
hoelzl |
alternative definition of conditional entropy
|
changeset |
files
|
| Wed, 10 Oct 2012 12:12:27 +0200 |
hoelzl |
remove unneeded assumption from conditional_entropy_generic_eq
|
changeset |
files
|
| Wed, 10 Oct 2012 12:12:27 +0200 |
hoelzl |
add induction rule for intersection-stable sigma-sets
|
changeset |
files
|