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