| Fri, 04 Jan 2013 21:24:47 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Fri, 04 Jan 2013 21:16:08 +0100 |
wenzelm |
more reactive completion popup by default;
|
file |
diff |
annotate
|
| Fri, 04 Jan 2013 19:00:49 +0100 |
blanchet |
updated docs
|
file |
diff |
annotate
|
| Fri, 04 Jan 2013 13:03:21 +0100 |
wenzelm |
more NEWS;
|
file |
diff |
annotate
|
| Fri, 04 Jan 2013 12:44:47 +0100 |
wenzelm |
document 'locale_deps';
|
file |
diff |
annotate
|
| Thu, 03 Jan 2013 14:23:10 +0100 |
wenzelm |
NEWS: ML runtime statistics;
|
file |
diff |
annotate
|
| Mon, 31 Dec 2012 13:08:37 +0100 |
wenzelm |
misc tuning for release;
|
file |
diff |
annotate
|
| Mon, 31 Dec 2012 12:25:11 +0100 |
wenzelm |
recovered Isabelle2012 NEWS from ae12b92c145a, except for e5420161d11d;
|
file |
diff |
annotate
|
| Sat, 29 Dec 2012 17:18:01 +0100 |
nipkow |
new theory Library/Finite_Lattice
|
file |
diff |
annotate
|
| Sun, 23 Dec 2012 19:54:15 +0100 |
nipkow |
renamed and added lemmas
|
file |
diff |
annotate
|
| Tue, 18 Dec 2012 21:59:44 +0100 |
haftmann |
discontinued legacy antiquotations and styles
|
file |
diff |
annotate
|
| Fri, 14 Dec 2012 15:46:01 +0100 |
hoelzl |
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
|
file |
diff |
annotate
|
| Fri, 14 Dec 2012 14:46:01 +0100 |
hoelzl |
NEWS
|
file |
diff |
annotate
|
| Fri, 14 Dec 2012 12:40:07 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Thu, 13 Dec 2012 13:11:38 +0100 |
Christian Sternagel |
renamed "emb" to "list_hembeq";
|
file |
diff |
annotate
|
| Thu, 13 Dec 2012 19:53:55 +0100 |
wenzelm |
smarter handling of tracing messages: prover process pauses and enters user dialog;
|
file |
diff |
annotate
|
| Mon, 10 Dec 2012 16:06:57 +0100 |
wenzelm |
more generous tracing limit -- rescaled in MB;
|
file |
diff |
annotate
|
| Thu, 06 Dec 2012 21:46:20 +0100 |
wenzelm |
documentation for isabelle build_dialog and its implicit use in isabelle jedit;
|
file |
diff |
annotate
|
| Mon, 26 Nov 2012 19:53:43 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 26 Nov 2012 17:13:44 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Mon, 26 Nov 2012 11:46:19 +0100 |
blanchet |
updated NEWS etc.
|
file |
diff |
annotate
|
| Mon, 26 Nov 2012 13:54:43 +0100 |
wenzelm |
refined outer syntax 'help' command;
|
file |
diff |
annotate
|
| Sun, 25 Nov 2012 17:15:21 +0100 |
wenzelm |
added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
|
file |
diff |
annotate
|
| Sat, 24 Nov 2012 15:49:43 +0100 |
wenzelm |
more NEWS/CONTRIBUTORS;
|
file |
diff |
annotate
|
| Sat, 24 Nov 2012 14:50:19 +0100 |
wenzelm |
improved editing support for control styles;
|
file |
diff |
annotate
|
| Sat, 24 Nov 2012 12:39:58 +0100 |
wenzelm |
added ISABELLE_PLATFORM_FAMILY;
|
file |
diff |
annotate
|
| Wed, 21 Nov 2012 10:57:50 +0100 |
hoelzl |
NEWS: document changes in HOL-Probability
|
file |
diff |
annotate
|
| Wed, 21 Nov 2012 10:48:58 +0100 |
hoelzl |
NEWS (changeset 13211e07d931): add Countable_Set
|
file |
diff |
annotate
|
| Wed, 21 Nov 2012 10:48:22 +0100 |
hoelzl |
NEWS (changeset 69b35a75caf3): document changes in FuncSet
|
file |
diff |
annotate
|
| Wed, 21 Nov 2012 09:07:41 +0100 |
nipkow |
new theory of immutable arrays
|
file |
diff |
annotate
|
| Tue, 20 Nov 2012 15:18:11 +0100 |
wenzelm |
simplified command line of "isabelle install";
|
file |
diff |
annotate
|
| Mon, 19 Nov 2012 20:23:47 +0100 |
wenzelm |
theorem status about oracles/futures is no longer printed by default;
|
file |
diff |
annotate
|
| Sun, 18 Nov 2012 16:04:13 +0100 |
wenzelm |
more generous tracing_limit, with explicit system option;
|
file |
diff |
annotate
|
| Sun, 18 Nov 2012 15:38:37 +0100 |
wenzelm |
adjust max_threads_value to capabilities of Poly/ML 5.5 and current hardware;
|
file |
diff |
annotate
|
| Sat, 17 Nov 2012 20:19:34 +0100 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Thu, 08 Nov 2012 19:55:19 +0100 |
bulwahn |
NEWS
|
file |
diff |
annotate
|
| Tue, 06 Nov 2012 15:15:33 +0100 |
blanchet |
renamed Sledgehammer option
|
file |
diff |
annotate
|
| Mon, 22 Oct 2012 22:24:34 +0200 |
haftmann |
incorporated constant chars into instantiation proof for enum;
|
file |
diff |
annotate
|
| Mon, 22 Oct 2012 14:52:38 +0200 |
wenzelm |
more detailed Prover IDE NEWS;
|
file |
diff |
annotate
|
| Sun, 21 Oct 2012 17:04:13 +0200 |
webertj |
merged
|
file |
diff |
annotate
|
| Fri, 19 Oct 2012 15:12:52 +0200 |
webertj |
Renamed {left,right}_distrib to distrib_{right,left}.
|
file |
diff |
annotate
|
| Sat, 20 Oct 2012 09:12:16 +0200 |
haftmann |
moved quite generic material from theory Enum to more appropriate places
|
file |
diff |
annotate
|
| Thu, 18 Oct 2012 15:05:17 +0200 |
blanchet |
renamed Isar-proof related options + changed semantics of Isar shrinking
|
file |
diff |
annotate
|
| Tue, 16 Oct 2012 21:30:52 +0200 |
wenzelm |
support for more informative errors in lazy enumerations;
|
file |
diff |
annotate
|
| Fri, 12 Oct 2012 22:10:45 +0200 |
wenzelm |
more NEWS;
|
file |
diff |
annotate
|
| Fri, 12 Oct 2012 21:39:58 +0200 |
wenzelm |
simplified 'typedef' specifications: discontinued implicit set definition and alternative name;
|
file |
diff |
annotate
|
| Thu, 11 Oct 2012 11:56:42 +0200 |
haftmann |
simplified construction of fold combinator on multisets;
|
file |
diff |
annotate
|
| Wed, 10 Oct 2012 13:03:50 +0200 |
Andreas Lochbihler |
efficient construction of red black trees from sorted associative lists
|
file |
diff |
annotate
|
| Mon, 08 Oct 2012 12:03:49 +0200 |
haftmann |
consolidated names of theorems on composition;
|
file |
diff |
annotate
|
| Mon, 08 Oct 2012 11:37:03 +0200 |
haftmann |
corrected NEWS
|
file |
diff |
annotate
|
| Thu, 04 Oct 2012 13:56:32 +0200 |
wenzelm |
some documentation of show_markup;
|
file |
diff |
annotate
|
| Fri, 28 Sep 2012 16:51:58 +0200 |
wenzelm |
smarter handling of tracing messages;
|
file |
diff |
annotate
|
| Sat, 22 Sep 2012 21:23:16 +0200 |
wenzelm |
some PIDE NEWS from this summer;
|
file |
diff |
annotate
|
| Fri, 21 Sep 2012 16:45:06 +0200 |
blanchet |
renamed "Codatatype" directory "BNF" (and corresponding session) -- this opens the door to no-nonsense session names like "HOL-BNF-LFP"
|
file |
diff |
annotate
|
| Thu, 20 Sep 2012 17:21:13 +0200 |
Andreas Lochbihler |
NEWS and CONTRIBUTORS for a5377f6d9f14 and f0ecc1550998
|
file |
diff |
annotate
|
| Sat, 15 Sep 2012 20:14:29 +0200 |
haftmann |
typeclass formalising bounded subtraction
|
file |
diff |
annotate
|
| Fri, 14 Sep 2012 12:09:27 +0200 |
blanchet |
merged two commands
|
file |
diff |
annotate
|
| Wed, 12 Sep 2012 05:29:21 +0200 |
blanchet |
renamed "Ordinals_and_Cardinals" to "Cardinals"
|
file |
diff |
annotate
|
| Mon, 10 Sep 2012 12:13:39 +0200 |
wenzelm |
more explicit indication of legacy features;
|
file |
diff |
annotate
|
| Fri, 07 Sep 2012 08:20:18 +0200 |
haftmann |
lattice instances for option type
|
file |
diff |
annotate
|
| Fri, 07 Sep 2012 08:20:18 +0200 |
haftmann |
combinator Option.these
|
file |
diff |
annotate
|
| Tue, 04 Sep 2012 13:06:28 +0900 |
Christian Sternagel |
NEWS; CONTRIBUTORS
|
file |
diff |
annotate
|
| Mon, 03 Sep 2012 11:09:25 +0200 |
wenzelm |
"isabelle logo" produces EPS and PDF format simultaneously;
|
file |
diff |
annotate
|
| Wed, 29 Aug 2012 20:16:22 +0200 |
wenzelm |
provide polyml-5.4.1 as regular component;
|
file |
diff |
annotate
|
| Wed, 29 Aug 2012 11:48:45 +0200 |
wenzelm |
renamed Position.str_of to Position.here;
|
file |
diff |
annotate
|
| Tue, 28 Aug 2012 17:17:25 +0200 |
blanchet |
updated NEWS and CONTRIBUTORS
|
file |
diff |
annotate
|
| Mon, 27 Aug 2012 16:10:54 +0200 |
wenzelm |
clarified "isabelle logo";
|
file |
diff |
annotate
|
| Wed, 22 Aug 2012 22:47:16 +0200 |
wenzelm |
'ML_file' evaluates ML text from a file directly within the theory, without predeclaration via 'uses';
|
file |
diff |
annotate
|
| Fri, 17 Aug 2012 17:35:07 +0200 |
wenzelm |
some explanations on isabelle components;
|
file |
diff |
annotate
|
| Tue, 14 Aug 2012 11:43:08 +0200 |
wenzelm |
support for 'typ' with explicit sort constraint;
|
file |
diff |
annotate
|
| Wed, 08 Aug 2012 14:45:40 +0200 |
wenzelm |
discontinued obsolete "isabelle makeall";
|
file |
diff |
annotate
|
| Tue, 07 Aug 2012 23:43:05 +0200 |
wenzelm |
discontinued obsolete IsaMakefile and ROOT.ML files from the Isabelle distribution;
|
file |
diff |
annotate
|
| Mon, 06 Aug 2012 16:05:29 +0200 |
wenzelm |
"isabelle options" prints Isabelle system options;
|
file |
diff |
annotate
|
| Sun, 05 Aug 2012 20:11:32 +0200 |
wenzelm |
more on isabelle mkroot;
|
file |
diff |
annotate
|
| Fri, 03 Aug 2012 12:37:31 +0200 |
wenzelm |
simplified custom document/build script, instead of old-style document/IsaMakefile;
|
file |
diff |
annotate
|
| Tue, 31 Jul 2012 16:23:20 +0200 |
wenzelm |
document variant NAME may use different LaTeX entry point document/root_NAME.tex if that file exists;
|
file |
diff |
annotate
|
| Sat, 28 Jul 2012 20:18:15 +0200 |
wenzelm |
discontinued obsolete Isabelle/build script;
|
file |
diff |
annotate
|
| Sat, 28 Jul 2012 20:12:47 +0200 |
wenzelm |
announce advanced support for Isabelle sessions and build management;
|
file |
diff |
annotate
|
| Sat, 28 Jul 2012 13:11:58 +0200 |
wenzelm |
discontinued special treatment of Proof General;
|
file |
diff |
annotate
|
| Mon, 23 Jul 2012 09:28:03 +0200 |
haftmann |
restrict unqualified imports from Haskell Prelude to a small set of fundamental operations
|
file |
diff |
annotate
|
| Sun, 22 Jul 2012 10:00:51 +0200 |
haftmann |
NEWS
|
file |
diff |
annotate
|
| Fri, 20 Jul 2012 22:19:46 +0200 |
blanchet |
added MaSh to news
|
file |
diff |
annotate
|
| Thu, 19 Jul 2012 22:21:59 +0200 |
haftmann |
export code relatively to master directory
|
file |
diff |
annotate
|
| Wed, 18 Jul 2012 08:44:04 +0200 |
blanchet |
removed lie
|
file |
diff |
annotate
|
| Wed, 18 Jul 2012 08:44:03 +0200 |
blanchet |
doc updates
|
file |
diff |
annotate
|
| Fri, 06 Jul 2012 16:31:37 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 06 Jul 2012 16:20:54 +0200 |
wenzelm |
discontinued obsolete attribute "COMP";
|
file |
diff |
annotate
|
| Fri, 29 Jun 2012 15:45:50 +0200 |
wenzelm |
default for \<euro> is now based on eurosym package, instead of slightly exotic babel/greek (which causes problems with the Gentoo installation on lxbroy2);
|
file |
diff |
annotate
|
| Mon, 25 Jun 2012 11:07:51 +0200 |
wenzelm |
updated "isar-ref" manual, reduced remaining material in "ref" manual.
|
file |
diff |
annotate
|
| Thu, 21 Jun 2012 13:51:44 +0200 |
bulwahn |
NEWS and CONTRIBUTORS
|
file |
diff |
annotate
|
| Wed, 06 Jun 2012 10:35:05 +0200 |
blanchet |
updated NEWS
|
file |
diff |
annotate
|
| Mon, 04 Jun 2012 09:07:23 +0200 |
boehmes |
restricted Z3 by default to a fragment where proof reconstruction should not fail (for better integration with Sledgehammer) -- the full set of supported Z3 features can still be used by enabling the configuration option "z3_with_extensions"
|
file |
diff |
annotate
|
| Tue, 29 May 2012 13:46:50 +0200 |
bulwahn |
added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
|
file |
diff |
annotate
|
| Thu, 24 May 2012 15:01:17 +0200 |
wenzelm |
discontinued support for Poly/ML 5.2.1;
|
file |
diff |
annotate
|
| Wed, 23 May 2012 16:22:27 +0200 |
wenzelm |
discontinued obsolete method fastsimp / tactic fast_simp_tac;
|
file |
diff |
annotate
|
| Wed, 23 May 2012 12:02:27 +0200 |
wenzelm |
merged, abandoning change of src/HOL/Tools/ATP/atp_problem_generate.ML from 6ea205a4d7fd;
|
file |
diff |
annotate
|
| Wed, 02 May 2012 22:05:59 +0200 |
wenzelm |
back to post-release mode -- after fork point;
|
file |
diff |
annotate
|
| Thu, 03 May 2012 22:07:29 +0200 |
wenzelm |
more NEWS;
|
file |
diff |
annotate
|
| Wed, 02 May 2012 20:43:57 +0200 |
wenzelm |
some re-ordering;
|
file |
diff |
annotate
|
| Wed, 02 May 2012 20:31:15 +0200 |
wenzelm |
some re-ordering;
|
file |
diff |
annotate
|
| Wed, 02 May 2012 20:15:31 +0200 |
wenzelm |
tuned spelling;
|
file |
diff |
annotate
|
| Wed, 02 May 2012 17:23:41 +0200 |
huffman |
edit NEWS items for transfer/lifting
|
file |
diff |
annotate
|
| Mon, 30 Apr 2012 22:18:39 +1000 |
Gerwin Klein |
provide [[record_codegen]] option for skipping codegen setup for records
|
file |
diff |
annotate
|
| Sat, 28 Apr 2012 18:09:50 +0200 |
wenzelm |
some re-ordering;
|
file |
diff |
annotate
|
| Sat, 28 Apr 2012 17:54:50 +0200 |
wenzelm |
updated system manual for release;
|
file |
diff |
annotate
|
| Sat, 28 Apr 2012 10:03:46 +0200 |
haftmann |
less confusion in NEWS
|
file |
diff |
annotate
|
| Fri, 27 Apr 2012 21:24:30 +0200 |
wenzelm |
mention tools and packages earlier;
|
file |
diff |
annotate
|
| Fri, 27 Apr 2012 21:13:55 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 27 Apr 2012 21:02:34 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 25 Apr 2012 14:28:13 +0200 |
hoelzl |
sorted lemma list in NEWS
|
file |
diff |
annotate
|
| Mon, 23 Apr 2012 22:22:57 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Mon, 23 Apr 2012 21:31:52 +0200 |
krauss |
NEWS
|
file |
diff |
annotate
|
| Mon, 23 Apr 2012 21:53:43 +0200 |
wenzelm |
typedef with implicit set definition is considered legacy;
|
file |
diff |
annotate
|
| Mon, 23 Apr 2012 12:14:35 +0200 |
hoelzl |
reworked Probability theory
|
file |
diff |
annotate
|
| Sun, 22 Apr 2012 16:33:41 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Sun, 22 Apr 2012 14:16:46 +0200 |
blanchet |
fixed typos
|
file |
diff |
annotate
|
| Sun, 22 Apr 2012 14:30:18 +0200 |
wenzelm |
USER_HOME settings variable points to cross-platform user home directory;
|
file |
diff |
annotate
|
| Sat, 21 Apr 2012 21:38:08 +0200 |
huffman |
update NEWS for transfer/quotient
|
file |
diff |
annotate
|
| Sat, 21 Apr 2012 13:54:29 +0200 |
huffman |
NEWS for transfer, lifting, and quotient
|
file |
diff |
annotate
|
| Fri, 20 Apr 2012 11:17:01 +0200 |
hoelzl |
NEWS
|
file |
diff |
annotate
|