Wed, 04 Jul 2018 22:44:24 +0200 |
wenzelm |
more frugal single-assignment according to David Matthews: dispose mutable lock/cond eventually;
|
changeset |
files
|
Wed, 04 Jul 2018 14:26:27 +0200 |
Lars Hupel |
merged
|
changeset |
files
|
Wed, 04 Jul 2018 10:58:28 +0200 |
Lars Hupel |
avoid clashes in quickcheck [random]
|
changeset |
files
|
Wed, 04 Jul 2018 11:00:06 +0100 |
paulson |
infinite products: the final piece
|
changeset |
files
|
Tue, 03 Jul 2018 14:46:14 +0100 |
paulson |
more on infinite products
|
changeset |
files
|
Tue, 03 Jul 2018 10:07:35 +0100 |
paulson |
merged
|
changeset |
files
|
Tue, 03 Jul 2018 10:07:24 +0100 |
paulson |
even more from Paulo
|
changeset |
files
|
Tue, 03 Jul 2018 11:00:37 +0200 |
wenzelm |
more standard headers;
|
changeset |
files
|
Tue, 03 Jul 2018 10:49:44 +0200 |
wenzelm |
eliminated hard TABs, assuming tabsize=8;
|
changeset |
files
|
Tue, 03 Jul 2018 00:15:16 +0100 |
paulson |
more latex problems
|
changeset |
files
|
Mon, 02 Jul 2018 23:06:34 +0100 |
paulson |
latex fixes
|
changeset |
files
|
Mon, 02 Jul 2018 22:40:25 +0100 |
paulson |
more algebra
|
changeset |
files
|
Mon, 02 Jul 2018 21:45:35 +0100 |
paulson |
merged
|
changeset |
files
|
Mon, 02 Jul 2018 21:45:10 +0100 |
paulson |
Hiding the constant "norm", lest it clash with the norm of a vector space
|
changeset |
files
|
Mon, 02 Jul 2018 18:58:50 +0100 |
paulson |
more lemmas from Paulo
|
changeset |
files
|
Mon, 02 Jul 2018 20:28:09 +0200 |
wenzelm |
merged
|
changeset |
files
|
Mon, 02 Jul 2018 16:48:00 +0200 |
wenzelm |
updated for release;
|
changeset |
files
|
Mon, 02 Jul 2018 16:43:06 +0200 |
wenzelm |
Added tag Isabelle2018-RC1 for changeset cf01d04e94d7
|
changeset |
files
|
Mon, 02 Jul 2018 16:20:03 +0100 |
paulson |
fixed (?) LaTeX presentation
|
changeset |
files
|
Mon, 02 Jul 2018 15:43:22 +0100 |
paulson |
merged
|
changeset |
files
|
Mon, 02 Jul 2018 14:41:35 +0100 |
paulson |
Lots of new algebra theories by Martin Baillon and Paulo EmÃlio de Vilhena
|
changeset |
files
|
Mon, 02 Jul 2018 16:26:11 +0200 |
wenzelm |
more NEWS;
|
changeset |
files
|
Mon, 02 Jul 2018 16:25:41 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
Mon, 02 Jul 2018 16:26:58 +0200 |
wenzelm |
more robust: avoid dire effect of ui.tweakoptions on hg.known_files;
|
changeset |
files
|
Mon, 02 Jul 2018 10:17:23 +0200 |
blanchet |
update Sledgehammer docs w.r.t. Vampire
|
changeset |
files
|
Mon, 02 Jul 2018 10:03:11 +0200 |
blanchet |
added Vampire component
|
changeset |
files
|
Mon, 02 Jul 2018 10:02:44 +0200 |
blanchet |
added option for noncommercial Vampire
|
changeset |
files
|
Sun, 01 Jul 2018 20:29:23 +0100 |
paulson |
merged
|
changeset |
files
|
Sun, 01 Jul 2018 20:28:47 +0100 |
paulson |
new lemmas, de-applying, etc.
|
changeset |
files
|
Sun, 01 Jul 2018 19:51:04 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
Sun, 01 Jul 2018 19:50:33 +0200 |
wenzelm |
merged
|
changeset |
files
|
Sun, 01 Jul 2018 12:38:37 +0200 |
wenzelm |
discontinued pending_shyps: too much complication due to lazy facts;
|
changeset |
files
|
Sun, 01 Jul 2018 12:37:24 +0200 |
wenzelm |
proper error;
|
changeset |
files
|
Sun, 01 Jul 2018 16:46:28 +0100 |
paulson |
merged
|
changeset |
files
|
Sun, 01 Jul 2018 16:13:25 +0100 |
paulson |
a few more lemmas from Paulo and Martin
|
changeset |
files
|
Sun, 01 Jul 2018 17:38:08 +0200 |
nipkow |
merged
|
changeset |
files
|
Sun, 01 Jul 2018 10:58:14 +0200 |
nipkow |
added lemmas
|
changeset |
files
|
Sat, 30 Jun 2018 18:58:13 +0100 |
paulson |
credits to Paulo and Martin
|
changeset |
files
|
Sat, 30 Jun 2018 15:44:04 +0100 |
paulson |
More on Algebra by Paulo and Martin
|
changeset |
files
|
Fri, 29 Jun 2018 23:04:36 +0200 |
Andreas Lochbihler |
merged
|
changeset |
files
|
Fri, 29 Jun 2018 22:56:34 +0200 |
Andreas Lochbihler |
declare case theorems as proper code equations
|
changeset |
files
|
Fri, 29 Jun 2018 22:50:35 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
Fri, 29 Jun 2018 22:14:33 +0200 |
wenzelm |
merged;
|
changeset |
files
|
Fri, 29 Jun 2018 20:32:24 +0200 |
wenzelm |
VSCode extension for official Isabelle release;
|
changeset |
files
|
Fri, 29 Jun 2018 20:11:17 +0200 |
wenzelm |
misc tuning and updates for release;
|
changeset |
files
|
Fri, 29 Jun 2018 19:53:15 +0200 |
wenzelm |
more manual tests;
|
changeset |
files
|
Fri, 29 Jun 2018 19:50:03 +0200 |
wenzelm |
misc tuning for release;
|
changeset |
files
|
Fri, 29 Jun 2018 16:53:37 +0200 |
wenzelm |
clarified error;
|
changeset |
files
|
Fri, 29 Jun 2018 16:45:54 +0200 |
wenzelm |
command-line option for include_sessions;
|
changeset |
files
|
Fri, 29 Jun 2018 15:54:41 +0200 |
wenzelm |
disallow pending hyps;
|
changeset |
files
|
Fri, 29 Jun 2018 14:19:52 +0200 |
wenzelm |
disallow hyps in export;
|
changeset |
files
|
Fri, 29 Jun 2018 14:02:14 +0200 |
wenzelm |
always consolidate: allow errors in presentation;
|
changeset |
files
|
Fri, 29 Jun 2018 11:36:31 +0200 |
wenzelm |
proper build_heap;
|
changeset |
files
|
Thu, 28 Jun 2018 21:05:56 +0200 |
wenzelm |
avoid pending shyps in global theory facts;
|
changeset |
files
|
Fri, 29 Jun 2018 15:22:30 +0100 |
paulson |
The unwinding number is an integer.
|
changeset |
files
|
Fri, 29 Jun 2018 14:00:37 +0100 |
paulson |
Now based on Complex_Main, not HOL.Deriv
|
changeset |
files
|
Fri, 29 Jun 2018 11:39:40 +0100 |
paulson |
merged
|
changeset |
files
|
Thu, 28 Jun 2018 17:14:40 +0100 |
paulson |
Incorporating new/strengthened proofs from Library and AFP entries
|
changeset |
files
|
Fri, 29 Jun 2018 10:55:05 +0100 |
Wenda Li |
NEWS and CONTRIBUTORS
|
changeset |
files
|
Fri, 29 Jun 2018 10:24:36 +0200 |
Lars Hupel |
remove trailing commas
|
changeset |
files
|
Thu, 28 Jun 2018 17:14:52 +0200 |
nipkow |
added lemmas
|
changeset |
files
|
Thu, 28 Jun 2018 14:14:05 +0100 |
paulson |
merged
|
changeset |
files
|
Thu, 28 Jun 2018 14:13:57 +0100 |
paulson |
Generalising and renaming some basic results
|
changeset |
files
|
Thu, 28 Jun 2018 13:49:02 +0200 |
immler |
transfer more lemmas
|
changeset |
files
|
Thu, 28 Jun 2018 13:18:02 +0200 |
immler |
fixed some oversights
|
changeset |
files
|
Thu, 28 Jun 2018 10:13:54 +0200 |
immler |
avoid duplicate facts, the "trick" was copied without deeper motivation
|
changeset |
files
|
Wed, 27 Jun 2018 20:31:22 +0200 |
wenzelm |
clarified settings -- avoid hard-wired directories;
|
changeset |
files
|
Wed, 27 Jun 2018 11:16:43 +0200 |
immler |
example for Types_To_Sets: transfer from type-based linear algebra to subspaces
|
changeset |
files
|
Wed, 27 Jun 2018 10:18:03 +0200 |
immler |
added lemmas and transfer rules
|
changeset |
files
|
Tue, 26 Jun 2018 23:39:28 +0200 |
wenzelm |
merged
|
changeset |
files
|
Tue, 26 Jun 2018 23:15:48 +0200 |
wenzelm |
smart_implode "$AFP" as well;
|
changeset |
files
|
Tue, 26 Jun 2018 21:59:05 +0100 |
paulson |
merged
|
changeset |
files
|
Tue, 26 Jun 2018 20:48:49 +0100 |
paulson |
a few new lemmas
|
changeset |
files
|
Tue, 26 Jun 2018 22:39:06 +0200 |
nipkow |
new theory Trie
|
changeset |
files
|
Tue, 26 Jun 2018 19:29:14 +0200 |
wenzelm |
merged
|
changeset |
files
|
Tue, 26 Jun 2018 19:17:11 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
Tue, 26 Jun 2018 19:16:14 +0200 |
wenzelm |
updated documentation;
|
changeset |
files
|
Tue, 26 Jun 2018 19:03:13 +0200 |
wenzelm |
clarified syntax;
|
changeset |
files
|
Tue, 26 Jun 2018 18:44:51 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
Tue, 26 Jun 2018 17:42:49 +0200 |
wenzelm |
simplified: allow only command names, with dummy for default;
|
changeset |
files
|
Tue, 26 Jun 2018 17:25:57 +0200 |
wenzelm |
clarified: more uniform keyword_tags;
|
changeset |
files
|
Tue, 26 Jun 2018 17:24:13 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
Tue, 26 Jun 2018 16:35:05 +0200 |
wenzelm |
more flexible document_tags;
|
changeset |
files
|
Tue, 26 Jun 2018 14:39:49 +0200 |
wenzelm |
prefer explicit options;
|
changeset |
files
|
Tue, 26 Jun 2018 14:01:46 +0200 |
wenzelm |
clarified default tag;
|
changeset |
files
|
Tue, 26 Jun 2018 11:11:05 +0200 |
wenzelm |
add URL;
|
changeset |
files
|
Tue, 26 Jun 2018 11:10:47 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
Tue, 26 Jun 2018 17:22:43 +0200 |
kleing |
more explicit statement of rat_denum to fit with top100 thms list
|
changeset |
files
|
Tue, 26 Jun 2018 15:44:35 +0100 |
paulson |
deleted redundant theorem
|
changeset |
files
|
Tue, 26 Jun 2018 14:51:32 +0100 |
paulson |
merged
|
changeset |
files
|
Tue, 26 Jun 2018 14:51:18 +0100 |
paulson |
Rationalisation of complex transcendentals, esp the Arg function
|
changeset |
files
|
Tue, 26 Jun 2018 15:16:22 +0200 |
Lars Hupel |
support NUMA shuffling in CI
|
changeset |
files
|
Tue, 26 Jun 2018 10:49:37 +0200 |
wenzelm |
merged
|
changeset |
files
|
Mon, 25 Jun 2018 17:18:55 +0200 |
wenzelm |
more scalable output;
|
changeset |
files
|
Mon, 25 Jun 2018 17:18:59 +0200 |
Lars Hupel |
obsolete
|
changeset |
files
|
Mon, 25 Jun 2018 14:06:50 +0100 |
paulson |
merged
|
changeset |
files
|