| Wed, 07 Sep 2011 11:26:27 +0200 |
wenzelm |
more NEWS;
|
file |
diff |
annotate
|
| Tue, 06 Sep 2011 21:56:11 +0200 |
wenzelm |
some Isabelle/jEdit NEWS;
|
file |
diff |
annotate
|
| Tue, 06 Sep 2011 07:48:59 -0700 |
huffman |
remove redundant lemma real_sum_squared_expand in favor of power2_sum
|
file |
diff |
annotate
|
| Tue, 06 Sep 2011 07:45:18 -0700 |
huffman |
remove redundant lemma LIMSEQ_Complex in favor of tendsto_Complex
|
file |
diff |
annotate
|
| Sun, 04 Sep 2011 10:05:52 -0700 |
huffman |
remove redundant lemmas expi_add and expi_zero
|
file |
diff |
annotate
|
| Sun, 04 Sep 2011 09:49:45 -0700 |
huffman |
remove redundant lemmas about LIMSEQ
|
file |
diff |
annotate
|
| Sat, 03 Sep 2011 09:26:11 -0700 |
huffman |
remove duplicate lemma finite_choice in favor of finite_set_choice
|
file |
diff |
annotate
|
| Fri, 02 Sep 2011 16:48:30 -0700 |
huffman |
remove redundant lemma reals_complete2 in favor of complete_real
|
file |
diff |
annotate
|
| Fri, 02 Sep 2011 13:57:12 -0700 |
huffman |
remove more duplicate lemmas
|
file |
diff |
annotate
|
| Thu, 01 Sep 2011 10:41:19 -0700 |
huffman |
simplify some proofs about uniform continuity, and add some new ones;
|
file |
diff |
annotate
|
| Thu, 01 Sep 2011 09:02:14 -0700 |
huffman |
modernize lemmas about 'continuous' and 'continuous_on';
|
file |
diff |
annotate
|
| Sun, 28 Aug 2011 09:20:12 -0700 |
huffman |
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
|
file |
diff |
annotate
|
| Fri, 26 Aug 2011 15:11:26 -0700 |
huffman |
NEWS entry for setsum_norm ~> norm_setsum
|
file |
diff |
annotate
|
| Thu, 25 Aug 2011 19:41:38 -0700 |
huffman |
replace some continuous_on lemmas with more general versions
|
file |
diff |
annotate
|
| Thu, 25 Aug 2011 16:50:55 -0700 |
huffman |
remove legacy theorem Lim_inner
|
file |
diff |
annotate
|
| Thu, 25 Aug 2011 15:35:54 -0700 |
huffman |
remove dot_lsum and dot_rsum in favor of inner_setsum_{left,right}
|
file |
diff |
annotate
|
| Thu, 25 Aug 2011 12:43:55 -0700 |
huffman |
rename subset_{interior,closure} to {interior,closure}_mono;
|
file |
diff |
annotate
|
| Fri, 19 Aug 2011 19:33:31 +0200 |
haftmann |
more concise definition for Inf, Sup on bool
|
file |
diff |
annotate
|
| Thu, 18 Aug 2011 13:36:58 -0700 |
huffman |
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
|
file |
diff |
annotate
|
| Thu, 18 Aug 2011 17:42:18 +0200 |
nipkow |
case_names NEWS
|
file |
diff |
annotate
|
| Wed, 10 Aug 2011 13:13:37 -0700 |
huffman |
more uniform naming scheme for finite cartesian product type and related theorems
|
file |
diff |
annotate
|
| Tue, 09 Aug 2011 08:06:15 +0200 |
haftmann |
more uniform naming scheme for Inf/INF and Sup/SUP lemmas
|
file |
diff |
annotate
|
| Tue, 09 Aug 2011 07:44:17 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
| Mon, 08 Aug 2011 19:21:11 +0200 |
haftmann |
dropped lemmas (Inf|Sup)_(singleton|binary)
|
file |
diff |
annotate
|
| Mon, 08 Aug 2011 19:26:53 -0700 |
huffman |
rename type 'a net to 'a filter, following standard mathematical terminology
|
file |
diff |
annotate
|
| Thu, 04 Aug 2011 07:31:43 +0200 |
haftmann |
NEWS
|
file |
diff |
annotate
|
| Wed, 03 Aug 2011 16:08:02 +0200 |
bulwahn |
NEWS
|
file |
diff |
annotate
|
| Tue, 02 Aug 2011 08:28:34 -0700 |
huffman |
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
|
file |
diff |
annotate
|
| Tue, 02 Aug 2011 07:36:58 -0700 |
huffman |
NEWS: fix typo
|
file |
diff |
annotate
|
| Tue, 02 Aug 2011 12:17:48 +0200 |
krauss |
NEWS
|
file |
diff |
annotate
|
| Mon, 25 Jul 2011 23:27:20 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
| Sun, 24 Jul 2011 21:27:25 +0200 |
haftmann |
more coherent structure in and across theories
|
file |
diff |
annotate
|
| Mon, 25 Jul 2011 10:42:32 +0200 |
bulwahn |
NEWS
|
file |
diff |
annotate
|
| Wed, 20 Jul 2011 22:14:39 +0200 |
haftmann |
class complete_linorder
|
file |
diff |
annotate
|
| Mon, 18 Jul 2011 21:34:01 +0200 |
haftmann |
avoid misunderstandable names
|
file |
diff |
annotate
|
| Sun, 17 Jul 2011 22:24:08 +0200 |
haftmann |
more on complement
|
file |
diff |
annotate
|
| Sun, 17 Jul 2011 20:57:56 +0200 |
haftmann |
more consistent theorem names
|
file |
diff |
annotate
|
| Sun, 17 Jul 2011 15:15:58 +0200 |
haftmann |
further generalization from sets to complete lattices
|
file |
diff |
annotate
|
| Wed, 13 Jul 2011 23:49:56 +0200 |
haftmann |
uniqueness lemmas for bot and top
|
file |
diff |
annotate
|
| Wed, 13 Jul 2011 23:41:13 +0200 |
haftmann |
adjusted to tightened specification of classes bot and top
|
file |
diff |
annotate
|
| Mon, 11 Jul 2011 17:22:15 +0200 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Sun, 10 Jul 2011 21:46:41 +0200 |
wenzelm |
merged;
|
file |
diff |
annotate
|
| Sun, 10 Jul 2011 14:02:27 +0200 |
bulwahn |
improved NEWS
|
file |
diff |
annotate
|
| Sat, 09 Jul 2011 21:18:20 +0200 |
bulwahn |
NEWS
|
file |
diff |
annotate
|
| Sun, 10 Jul 2011 20:59:04 +0200 |
wenzelm |
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
|
file |
diff |
annotate
|
| Fri, 08 Jul 2011 16:13:34 +0200 |
wenzelm |
discontinued special treatment of hard tabulators;
|
file |
diff |
annotate
|
| Fri, 01 Jul 2011 15:53:38 +0200 |
blanchet |
update documentation after "type_enc" renaming + fixed a few other out-of-date factlets
|
file |
diff |
annotate
|
| Fri, 01 Jul 2011 10:45:51 +0200 |
bulwahn |
adding a minimalistic documentation of the value antiquotation in the Isar reference manual
|
file |
diff |
annotate
|
| Mon, 27 Jun 2011 22:44:44 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Mon, 27 Jun 2011 14:56:29 +0200 |
blanchet |
minor Sledgehammer news
|
file |
diff |
annotate
|
| Mon, 27 Jun 2011 14:56:10 +0200 |
blanchet |
document changes to Sledgehammer and "try"
|
file |
diff |
annotate
|
| Mon, 27 Jun 2011 22:23:44 +0200 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Thu, 23 Jun 2011 12:02:54 +0200 |
ballarin |
Release notes should be written from the user's perspective. Don't assume the user has universal knowledge of the system.
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 10:43:42 +0200 |
bulwahn |
NEWS
|
file |
diff |
annotate
|
| Tue, 07 Jun 2011 08:52:35 +0200 |
blanchet |
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
|
file |
diff |
annotate
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
marked "metisF" as legacy -- nobody uses it or needs it
|
file |
diff |
annotate
|
| Fri, 20 May 2011 20:44:03 +0200 |
wenzelm |
added Isabelle_Process.is_active;
|
file |
diff |
annotate
|
| Fri, 20 May 2011 12:09:54 +0200 |
haftmann |
NEWS
|
file |
diff |
annotate
|
| Wed, 18 May 2011 15:45:34 +0200 |
bulwahn |
NEWS
|
file |
diff |
annotate
|
| Sun, 15 May 2011 18:00:08 +0200 |
wenzelm |
NEWS (cf. 4e8483cc2cc5);
|
file |
diff |
annotate
|
| Sat, 14 May 2011 18:26:25 +0200 |
haftmann |
use pointfree characterisation for fold_set locale
|
file |
diff |
annotate
|
| Fri, 13 May 2011 22:55:00 +0200 |
wenzelm |
proper Proof.context for classical tactics;
|
file |
diff |
annotate
|
| Thu, 12 May 2011 15:29:19 +0200 |
blanchet |
renamed "max_mono_instances" to "max_new_mono_instances" and changed its semantics accordingly
|
file |
diff |
annotate
|
| Thu, 12 May 2011 15:29:18 +0200 |
blanchet |
added "max_mono_instances" option to Sledgehammer and renamed old "monomorphize_limit" option
|
file |
diff |
annotate
|
| Thu, 05 May 2011 23:54:06 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 03 May 2011 22:27:32 +0200 |
wenzelm |
more conventional naming scheme: names_long, names_short, names_unique;
|
file |
diff |
annotate
|
| Tue, 03 May 2011 18:04:05 +0200 |
wenzelm |
some documentation of @{rail} antiquotation;
|
file |
diff |
annotate
|
| Mon, 02 May 2011 22:03:18 +0200 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Sun, 01 May 2011 18:37:25 +0200 |
blanchet |
document new type system syntax
|
file |
diff |
annotate
|
| Sun, 01 May 2011 17:13:44 +0200 |
wenzelm |
localized \isabellestyle;
|
file |
diff |
annotate
|
| Thu, 28 Apr 2011 21:06:04 +0200 |
wenzelm |
literal facts `prop` may contain dummy patterns;
|
file |
diff |
annotate
|
| Wed, 27 Apr 2011 13:21:12 +0200 |
wenzelm |
predefined LaTeX macros for \<bind> and \<then>;
|
file |
diff |
annotate
|
| Tue, 19 Apr 2011 15:58:05 +0200 |
wenzelm |
slightly more special eq_list/eq_set, with shortcut involving pointer_eq;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 22:21:34 +0200 |
wenzelm |
refined PARALLEL_GOALS;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 15:47:52 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 13:48:45 +0200 |
wenzelm |
Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 16:34:14 +0200 |
wenzelm |
discontinued special treatment of structure Lexicon;
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 13:31:16 +0200 |
wenzelm |
explicit structure Syntax_Trans;
|
file |
diff |
annotate
|
| Wed, 06 Apr 2011 13:33:46 +0200 |
wenzelm |
typed_print_translation: discontinued show_sorts argument;
|
file |
diff |
annotate
|
| Tue, 05 Apr 2011 15:15:33 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Mon, 04 Apr 2011 19:09:10 +0200 |
blanchet |
document "type_sys" option
|
file |
diff |
annotate
|
| Tue, 05 Apr 2011 14:25:18 +0200 |
wenzelm |
discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
|
file |
diff |
annotate
|
| Thu, 31 Mar 2011 11:16:52 +0200 |
blanchet |
added monomorphization option to Sledgehammer ATPs -- this looks promising but is still off by default
|
file |
diff |
annotate
|
| Wed, 30 Mar 2011 09:44:17 +0200 |
bulwahn |
NEWS
|
file |
diff |
annotate
|
| Tue, 29 Mar 2011 14:27:44 +0200 |
hoelzl |
NEWS
|
file |
diff |
annotate
|
| Tue, 22 Mar 2011 20:44:47 +0100 |
wenzelm |
more selective strip_positions in case patterns -- reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF;
|
file |
diff |
annotate
|
| Tue, 22 Mar 2011 18:03:28 +0100 |
wenzelm |
enable inner syntax source positions by default (controlled via configuration option);
|
file |
diff |
annotate
|
| Sun, 20 Mar 2011 22:26:43 +0100 |
wenzelm |
NEWS: structure Timing provides various operations for timing;
|
file |
diff |
annotate
|
| Fri, 18 Mar 2011 22:55:28 +0100 |
blanchet |
added "simp:", "intro:", and "elim:" to "try" command
|
file |
diff |
annotate
|
| Thu, 17 Mar 2011 22:07:17 +0100 |
blanchet |
reintroduced "show_skolems" option -- useful when too many Skolems are displayed
|
file |
diff |
annotate
|
| Sun, 13 Mar 2011 20:56:00 +0100 |
wenzelm |
files are identified via SHA1 digests -- discontinued ISABELLE_FILE_IDENT;
|
file |
diff |
annotate
|
| Sun, 13 Mar 2011 19:16:19 +0100 |
wenzelm |
cleanup of former settings GHC_PATH, EXEC_GHC, EXEC_OCAML, EXEC_SWIPL, EXEC_YAP -- discontinued implicit detection;
|
file |
diff |
annotate
|
| Sun, 13 Mar 2011 17:28:14 +0100 |
wenzelm |
clarified ISABELLE_CSDP setting (formerly CSDP_EXE);
|
file |
diff |
annotate
|
| Sun, 13 Mar 2011 16:01:00 +0100 |
wenzelm |
Path.print is the official way to show file-system paths to users -- note that Path.implode often indicates violation of the abstract datatype;
|
file |
diff |
annotate
|
| Thu, 03 Mar 2011 18:10:28 +0100 |
wenzelm |
discontinued legacy load path;
|
file |
diff |
annotate
|
| Thu, 03 Mar 2011 11:20:48 +0100 |
blanchet |
mention new Nitpick options
|
file |
diff |
annotate
|
| Fri, 25 Feb 2011 16:59:48 +0100 |
krauss |
removed support for tail-recursion from function package (now implemented by partial_function)
|
file |
diff |
annotate
|
| Mon, 21 Feb 2011 10:44:19 +0100 |
blanchet |
renamed "nitpick\_def" to "nitpick_unfold" to reflect its new semantics
|
file |
diff |
annotate
|
| Tue, 08 Feb 2011 21:12:27 +0100 |
wenzelm |
discontinued obsolete lib/scripts/polyml-platform;
|
file |
diff |
annotate
|
| Tue, 08 Feb 2011 17:38:43 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Tue, 08 Feb 2011 16:10:10 +0100 |
blanchet |
available_provers ~> supported_provers (for clarity)
|
file |
diff |
annotate
|
| Tue, 08 Feb 2011 17:36:21 +0100 |
wenzelm |
discontinued support for Poly/ML 5.2, which was the last version without proper multithreading and TimeLimit implementation;
|
file |
diff |
annotate
|
| Fri, 04 Feb 2011 17:11:00 +0100 |
wenzelm |
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
|
file |
diff |
annotate
|
| Tue, 01 Feb 2011 21:09:52 +0100 |
krauss |
term style 'isub': ad-hoc subscripting of variables that end with digits (x1, x23, ...)
|
file |
diff |
annotate
|
| Mon, 31 Jan 2011 11:18:29 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Mon, 17 Jan 2011 20:20:51 +0100 |
wenzelm |
back to post-release mode;
|
file |
diff |
annotate
|
| Wed, 19 Jan 2011 11:27:56 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 17 Jan 2011 18:32:16 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 17 Jan 2011 17:45:52 +0100 |
boehmes |
made Z3 the default SMT solver again
|
file |
diff |
annotate
|
| Sun, 16 Jan 2011 21:10:30 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 16 Jan 2011 20:55:48 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 16 Jan 2011 20:54:30 +0100 |
wenzelm |
misc tuning for release;
|
file |
diff |
annotate
|
| Sat, 15 Jan 2011 14:56:57 +0100 |
wenzelm |
global "prems" is legacy feature;
|
file |
diff |
annotate
|
| Sat, 15 Jan 2011 14:19:37 +0100 |
wenzelm |
misc updates for release;
|
file |
diff |
annotate
|
| Sat, 15 Jan 2011 14:02:24 +0100 |
wenzelm |
merged;
|
file |
diff |
annotate
|
| Sat, 15 Jan 2011 13:34:10 +0100 |
wenzelm |
misc tuning for release;
|
file |
diff |
annotate
|
| Sat, 15 Jan 2011 12:49:10 +0100 |
berghofe |
Added entry for HOL-SPARK
|
file |
diff |
annotate
|
| Tue, 11 Jan 2011 20:01:57 +0100 |
wenzelm |
updated to Isabelle2011;
|
file |
diff |
annotate
|
| Tue, 11 Jan 2011 18:23:29 +0100 |
haftmann |
NEWS
|
file |
diff |
annotate
|
| Tue, 11 Jan 2011 17:59:35 +0100 |
bulwahn |
NEWS
|
file |
diff |
annotate
|