| 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
|