| Thu, 17 Aug 2017 21:12:55 +0200 |
wenzelm |
support for incremental update according to session graph structure;
|
file |
diff |
annotate
|
| Tue, 15 Aug 2017 22:23:16 +0200 |
nipkow |
NEWS sorted_wrt
|
file |
diff |
annotate
|
| Tue, 15 Aug 2017 11:41:58 +0200 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Sun, 06 Aug 2017 15:02:54 +0200 |
haftmann |
do not fall back on nbe if plain evaluation fails
|
file |
diff |
annotate
|
| Wed, 02 Aug 2017 20:33:39 +0200 |
haftmann |
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
|
file |
diff |
annotate
|
| Fri, 28 Jul 2017 15:36:32 +0100 |
blanchet |
introduced option for nat-as-int in SMT
|
file |
diff |
annotate
|
| Sat, 15 Jul 2017 14:36:30 +0100 |
eberlm |
Updated NEWS
|
file |
diff |
annotate
|
| Mon, 03 Jul 2017 13:51:55 +0200 |
wenzelm |
added command 'alias' and 'type_alias';
|
file |
diff |
annotate
|
| Fri, 30 Jun 2017 21:19:13 +0200 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Fri, 23 Jun 2017 22:04:14 +0200 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Tue, 20 Jun 2017 13:07:49 +0200 |
haftmann |
deleting a code equation never leads to unimplemented function
|
file |
diff |
annotate
|
| Tue, 20 Jun 2017 14:41:29 +0200 |
blanchet |
SMT news
|
file |
diff |
annotate
|
| Mon, 05 Jun 2017 23:55:58 +0200 |
wenzelm |
HTML preview via builtin HTTP server;
|
file |
diff |
annotate
|
| Mon, 29 May 2017 09:14:15 +0200 |
eberlm |
reorganised material on sublists
|
file |
diff |
annotate
|
| Mon, 15 May 2017 17:05:52 +0200 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Fri, 05 May 2017 11:16:13 +0200 |
Manuel Eberl |
NEWS: totient 1 = 1 now
|
file |
diff |
annotate
|
| Mon, 24 Apr 2017 15:56:25 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 24 Apr 2017 11:23:07 +0200 |
wenzelm |
clarified meaning of "isabelle jedit -R": avoid potential problems with all_known = true;
|
file |
diff |
annotate
|
| Sun, 23 Apr 2017 23:10:23 +0200 |
wenzelm |
tuned documentation;
|
file |
diff |
annotate
|
| Sun, 23 Apr 2017 15:59:51 +0200 |
wenzelm |
clarified tool name -- more official status;
|
file |
diff |
annotate
|
| Sat, 22 Apr 2017 22:01:35 +0200 |
wenzelm |
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
|
file |
diff |
annotate
|
| Fri, 21 Apr 2017 20:36:20 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Fri, 21 Apr 2017 18:57:30 +0200 |
wenzelm |
afford unconditional all_known = true (reverting ea42dfd95ec8), for practical usability of qualified imports from arbitrary sessions;
|
file |
diff |
annotate
|
| Thu, 20 Apr 2017 16:21:28 +0200 |
blanchet |
removed Old_SMT legacy module
|
file |
diff |
annotate
|
| Wed, 19 Apr 2017 16:24:59 +0200 |
wenzelm |
optionally explore all sessions -- potentially slow, e.g. for AFP;
|
file |
diff |
annotate
|
| Wed, 19 Apr 2017 16:22:20 +0200 |
wenzelm |
proper sections;
|
file |
diff |
annotate
|
| Tue, 18 Apr 2017 16:34:58 +0200 |
wenzelm |
exclude theories from other sessions;
|
file |
diff |
annotate
|
| Tue, 18 Apr 2017 14:51:46 +0200 |
wenzelm |
some documentation;
|
file |
diff |
annotate
|
| Wed, 12 Apr 2017 09:27:43 +0200 |
haftmann |
more fundamental euler's totient function on nat rather than int;
|
file |
diff |
annotate
|
| Sun, 09 Apr 2017 21:06:19 +0200 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Sun, 09 Apr 2017 20:17:00 +0200 |
wenzelm |
added system option record_proofs, which allows to build HOL-Proofs without special Proofs.thy;
|
file |
diff |
annotate
|
| Thu, 06 Apr 2017 21:37:13 +0200 |
haftmann |
session containing computational algebra
|
file |
diff |
annotate
|
| Tue, 04 Apr 2017 09:01:19 +0200 |
eberlm |
moved AFP material to Formal_Power_Series; renamed E/L/F in Formal_Power_Series
|
file |
diff |
annotate
|
| Sun, 19 Mar 2017 20:28:21 +0100 |
wenzelm |
updated to jedit-5.4.0;
|
file |
diff |
annotate
|
| Fri, 10 Mar 2017 13:47:35 +0100 |
haftmann |
restored surj as output abbreviation, amending 6af79184bef3
|
file |
diff |
annotate
|
| Thu, 02 Mar 2017 21:16:02 +0100 |
ballarin |
Knaster-Tarski fixed point theorem and Galois Connections.
|
file |
diff |
annotate
|
| Wed, 01 Mar 2017 11:26:19 +0100 |
wenzelm |
more uniform platform settings;
|
file |
diff |
annotate
|
| Tue, 28 Feb 2017 23:12:52 +0100 |
wenzelm |
more detailed platform information;
|
file |
diff |
annotate
|
| Tue, 28 Feb 2017 13:51:47 +0000 |
paulson |
Renamed ii to imaginary_unit in order to free up ii as a variable name. Also replaced some legacy def commands
|
file |
diff |
annotate
|
| Mon, 27 Feb 2017 17:17:26 +0000 |
paulson |
Some new lemmas thanks to Lukas Bulwahn. Also, NEWS.
|
file |
diff |
annotate
|
| Mon, 27 Feb 2017 00:00:28 +0100 |
wenzelm |
clarified defaults;
|
file |
diff |
annotate
|
| Sun, 26 Feb 2017 23:50:19 +0100 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Sun, 26 Feb 2017 13:22:14 +0100 |
haftmann |
re-established AFP entry for FinFuns as library
|
file |
diff |
annotate
|
| Fri, 24 Feb 2017 12:24:13 +0100 |
wenzelm |
avoid Unicode that conflicts with Isabelle symbol rendering;
|
file |
diff |
annotate
|
| Wed, 22 Feb 2017 20:33:53 +0100 |
haftmann |
more precise NEWS and CONTRIBUTORS
|
file |
diff |
annotate
|
| Wed, 22 Feb 2017 20:24:50 +0100 |
haftmann |
basic documentation for computations
|
file |
diff |
annotate
|
| Mon, 13 Feb 2017 16:03:53 +0100 |
fleury |
renaming multiset simprocs
|
file |
diff |
annotate
|
| Sat, 04 Feb 2017 21:15:11 +0100 |
wenzelm |
more uniform use of Reconstruct.clean_proof_of;
|
file |
diff |
annotate
|
| Tue, 17 Jan 2017 16:11:47 +0100 |
wenzelm |
removed some old ASCII syntax;
|
file |
diff |
annotate
|
| Sun, 15 Jan 2017 15:51:33 +0100 |
wenzelm |
clarified settings;
|
file |
diff |
annotate
|
| Sun, 15 Jan 2017 15:48:26 +0100 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Wed, 11 Jan 2017 16:43:31 +0100 |
blanchet |
generalized types in lemmas
|
file |
diff |
annotate
|
| Tue, 10 Jan 2017 16:53:05 +0100 |
wenzelm |
support "purge" operation on document model;
|
file |
diff |
annotate
|
| Mon, 09 Jan 2017 14:40:31 +0000 |
paulson |
Jordan Curve Theorem
|
file |
diff |
annotate
|
| Mon, 09 Jan 2017 00:08:18 +0100 |
wenzelm |
NEWS for VSCode;
|
file |
diff |
annotate
|
| Sun, 08 Jan 2017 19:34:44 +0100 |
wenzelm |
more documentation;
|
file |
diff |
annotate
|
| Wed, 04 Jan 2017 21:28:33 +0100 |
haftmann |
tuned NEWS
|
file |
diff |
annotate
|
| Wed, 04 Jan 2017 21:28:29 +0100 |
haftmann |
reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings
|
file |
diff |
annotate
|
| Wed, 04 Jan 2017 21:28:29 +0100 |
haftmann |
moved euclidean ring to HOL
|
file |
diff |
annotate
|
| Thu, 22 Dec 2016 08:43:30 +0100 |
haftmann |
proper logical constants
|
file |
diff |
annotate
|