| 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
|
| Wed, 21 Dec 2016 21:26:26 +0100 |
haftmann |
prefer existing logical constant over abbreviation
|
file |
diff |
annotate
|
| Wed, 21 Dec 2016 21:26:26 +0100 |
haftmann |
dropped aliasses
|
file |
diff |
annotate
|
| Sun, 18 Dec 2016 22:14:53 +0100 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Sun, 18 Dec 2016 21:58:13 +0100 |
wenzelm |
added isabelle jedit -R;
|
file |
diff |
annotate
|
| Sat, 17 Dec 2016 15:22:14 +0100 |
haftmann |
reoriented congruence rules in non-explosive direction
|
file |
diff |
annotate
|
| Mon, 12 Dec 2016 17:40:06 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Mon, 12 Dec 2016 11:33:14 +0100 |
wenzelm |
proper session HOL-Types_To_Sets;
|
file |
diff |
annotate
|
| Thu, 08 Dec 2016 17:22:51 +0100 |
bulwahn |
remove typo in bij_swap_compose_bij theorem name; tune proof
|
file |
diff |
annotate
|
| Tue, 29 Nov 2016 08:32:46 +0100 |
blanchet |
don't generate 'size_gen_o_map' property if its type variable is too limited anyway to be useful
|
file |
diff |
annotate
|
| Sun, 27 Nov 2016 20:25:38 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Sun, 27 Nov 2016 13:19:29 +0100 |
wenzelm |
NEWS for e6a3c55b929b;
|
file |
diff |
annotate
|
| Thu, 24 Nov 2016 11:33:55 +0100 |
haftmann |
clarified NEWS concerning Library/Poly_Deriv
|
file |
diff |
annotate
|
| Sun, 20 Nov 2016 20:12:42 +0100 |
wenzelm |
more on "Formal scopes and semantic selection";
|
file |
diff |
annotate
|