NEWS
Mon, 28 Jun 2021 20:10:23 +0200 Andreas Lochbihler move code setup from Cardinality to separate theory
Fri, 25 Jun 2021 21:14:57 +0200 wenzelm support for jEdit font substitution;
Wed, 23 Jun 2021 17:43:31 +0000 haftmann more default simp rules
Wed, 09 Jun 2021 18:04:22 +0000 haftmann global interpretation into nested targets
Wed, 09 Jun 2021 10:58:28 +0200 wenzelm NEWS;
Mon, 07 Jun 2021 14:41:04 +0200 wenzelm tuned;
Mon, 07 Jun 2021 14:40:22 +0200 wenzelm more formal theory and session names;
Mon, 07 Jun 2021 14:34:55 +0200 wenzelm proper NEWS after Isabelle2021;
Mon, 07 Jun 2021 11:42:05 +0200 wenzelm allow system option short form NAME for NAME=true for type string, not just bool;
Sun, 06 Jun 2021 15:49:39 +0000 haftmann moved more legacy to AFP
Fri, 28 May 2021 20:21:23 +0000 haftmann max word moved to Word_Lib in AFP
Mon, 24 May 2021 11:58:06 +0200 wenzelm clarified system_log: make this work independently of the particular "isabelle build" command-line (e.g. "isabelle mirabelle");
Sun, 23 May 2021 22:46:30 +0200 wenzelm syslog option for "isabelle build";
Sun, 23 May 2021 20:12:36 +0200 wenzelm NEWS;
Wed, 19 May 2021 13:19:37 +0200 wenzelm explicit option document_bibliography;
Wed, 19 May 2021 13:00:42 +0200 wenzelm discontinued obsolete "isabelle latex";
Wed, 19 May 2021 11:15:13 +0200 wenzelm clarified bash scripts, with public interfaces for user-defined Document_Build.Engine;
Tue, 18 May 2021 22:02:21 +0200 wenzelm option document_preprocessor;
Tue, 18 May 2021 15:46:03 +0200 wenzelm clarified treatment of Isabelle .sty files;
Tue, 18 May 2021 15:17:55 +0200 wenzelm option document_logo;
Mon, 17 May 2021 23:30:25 +0200 wenzelm option document_build refers to build engine in Isabelle/Scala;
Wed, 12 May 2021 17:05:29 +0000 haftmann explicit type class operations for type-specific implementations
Wed, 12 May 2021 17:05:28 +0000 haftmann obsolete
Tue, 11 May 2021 16:30:24 +0200 wenzelm clarified platforms;
Sun, 09 May 2021 05:48:50 +0000 haftmann more elementary swap
Wed, 05 May 2021 16:09:02 +0000 haftmann tuned theory structure
Wed, 05 May 2021 16:09:02 +0000 haftmann more appropriate location
Sun, 02 May 2021 17:38:49 +0200 wenzelm support nested cases;
Thu, 22 Apr 2021 10:11:11 +0200 wenzelm simplified typesetting of \<guillemotleft>...\<guillemotright>;
Fri, 16 Apr 2021 23:16:00 +0200 wenzelm support for conditional ML text;
Fri, 09 Apr 2021 22:06:59 +0200 wenzelm support for ML special forms: modified evaluation similar to Scheme;
Sat, 27 Mar 2021 18:01:41 +0100 wenzelm clarified output;
Sat, 27 Mar 2021 17:13:15 +0100 wenzelm support repository archives (without full .hg directory);
Thu, 25 Mar 2021 08:52:15 +0000 haftmann dedicated session for combinatorial material
Mon, 22 Mar 2021 17:33:08 +0100 wenzelm more NEWS;
Mon, 22 Mar 2021 10:49:51 +0000 haftmann more lemmas
Mon, 22 Mar 2021 00:07:55 +0100 wenzelm clarified package name (actually both pxfonts and txfonts exist and have this font);
Sun, 21 Mar 2021 23:56:54 +0100 wenzelm tuned;
Sun, 21 Mar 2021 23:03:31 +0100 wenzelm high-quality blackboard-bold fonts from "txmia" (package "txfonts");
Wed, 17 Mar 2021 22:24:57 +0100 wenzelm more Isabelle symbol definitions for Z Notation, based on https://github.com/isabelle-utp/Z_Toolkit 998c9f7880d3 by Simon Foster;
Sun, 14 Mar 2021 21:02:34 +0100 wenzelm removed spurious references to perl / libwww-perl;
Thu, 11 Mar 2021 07:05:38 +0000 haftmann avoid name clash
Thu, 11 Mar 2021 11:22:25 +0100 wenzelm tuned;
Tue, 09 Mar 2021 21:11:05 +0100 wenzelm proper type-setting of cartouches (requires T1);
Sun, 07 Mar 2021 08:24:24 +0100 haftmann follow corresponding precedence on sets
Sat, 06 Mar 2021 18:42:10 +0000 haftmann consolidated names
Fri, 05 Mar 2021 17:29:49 +0100 wenzelm clarified timeouts in Isabelle/ML;
Fri, 05 Mar 2021 10:30:54 +0100 haftmann typo
Mon, 01 Mar 2021 08:16:22 +0100 haftmann NEWS
Sat, 27 Feb 2021 22:17:56 +0100 wenzelm more Isabelle/ML/Scala operations;
Sat, 27 Feb 2021 21:36:58 +0100 wenzelm more Isabelle/ML/Scala operations;
Sat, 27 Feb 2021 21:01:07 +0100 wenzelm more Isabelle/ML/Scala operations;
Tue, 23 Feb 2021 23:00:08 +0100 wenzelm more on Isabelle_System.bash;
Tue, 23 Feb 2021 20:41:48 +0000 haftmann more specific name
Mon, 22 Feb 2021 23:31:59 +0100 wenzelm NEWS;
Mon, 22 Feb 2021 18:28:12 +0000 haftmann NEWS
Mon, 22 Feb 2021 07:49:48 +0000 haftmann get rid of traditional predicate
Fri, 19 Feb 2021 13:42:12 +0100 Manuel Eberl HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Sat, 13 Feb 2021 20:39:29 +0100 wenzelm tuned NEWS;
Sun, 07 Feb 2021 20:44:44 +0100 wenzelm updated for release;
Wed, 03 Feb 2021 20:18:34 +0100 wenzelm clarified links to external files, e.g. .pdf within .thy source document;
Tue, 26 Jan 2021 23:34:40 +0100 wenzelm more NEWS;
Fri, 22 Jan 2021 18:44:34 +0100 wenzelm IDE support for Naproche-SAD;
Thu, 21 Jan 2021 16:10:43 +0100 wenzelm support isabelle components -u and -x;
Tue, 19 Jan 2021 14:14:23 +0100 wenzelm clarified documentation concerning macOS Big Sur;
Mon, 18 Jan 2021 20:11:42 +0100 wenzelm obsolete;
Mon, 18 Jan 2021 19:53:20 +0100 wenzelm more NEWS;
Sun, 17 Jan 2021 11:19:15 +0100 wenzelm revert 1105c42722dc on isabelle-release branch;
Sun, 10 Jan 2021 15:48:15 +0100 wenzelm back to post-release mode;
Sun, 10 Jan 2021 15:35:24 +0100 wenzelm tuned;
Sun, 10 Jan 2021 13:17:27 +0100 wenzelm more documentation;
Sat, 09 Jan 2021 19:49:22 +0100 wenzelm clarified default L&F of Isabelle/Scala (not Isabelle/jEdit);
Sat, 09 Jan 2021 00:11:52 +0100 wenzelm clarified default L&F;
Fri, 08 Jan 2021 19:53:44 +0100 Manuel Eberl HOL-Data_Structures: added Selection and time functions for list functions
Thu, 07 Jan 2021 13:23:54 +0100 wenzelm clarified NEWS;
Wed, 06 Jan 2021 12:59:52 +0100 wenzelm more NEWS;
Tue, 05 Jan 2021 03:35:46 +0100 Manuel Eberl HOL-Library.Multiset: new notation for prod_mset, consistent with sum_mset
Mon, 04 Jan 2021 21:25:40 +0100 wenzelm merged
Mon, 04 Jan 2021 21:24:15 +0100 wenzelm more documentation;
Mon, 04 Jan 2021 19:41:38 +0100 Manuel Eberl HOL-Library: Changed notation for sum_mset
Sun, 27 Dec 2020 14:04:16 +0100 wenzelm tuned;
Sun, 27 Dec 2020 13:52:55 +0100 wenzelm proper NEWS according to current situation;
Sun, 27 Dec 2020 13:49:03 +0100 wenzelm updated for release;
Thu, 24 Dec 2020 00:07:51 +0100 wenzelm more NEWS;
Wed, 23 Dec 2020 21:06:31 +0100 wenzelm clarified modules: avoid multiple uses of the same ML file;
Mon, 21 Dec 2020 14:03:12 +0100 wenzelm misc tuning for release;
Mon, 21 Dec 2020 13:58:11 +0100 wenzelm rebuild component with proper ZIPPERPOSITION_HOME for sledgehammer;
Mon, 21 Dec 2020 12:51:28 +0100 wenzelm provide zipperposition-2.0 for experimentation;
Sat, 19 Dec 2020 00:08:14 +0100 wenzelm download auxiliary files via "curl";
Fri, 18 Dec 2020 23:19:07 +0100 wenzelm improved markup for theory header imports;
Wed, 16 Dec 2020 15:39:21 +0100 wenzelm more NEWS;
Wed, 16 Dec 2020 13:47:33 +0100 wenzelm added action isabelle.goto-entity to follow links in a narrow formal sense;
Thu, 10 Dec 2020 22:44:53 +0100 wenzelm clarified session log file: avoid erratic messages;
Thu, 10 Dec 2020 18:38:26 +0100 wenzelm NEWS and documentation for "isabelle log";
Sun, 06 Dec 2020 16:27:37 +0100 wenzelm PIDE support for session ROOTS;
Fri, 04 Dec 2020 18:29:48 +0100 nipkow NEWS
Sat, 28 Nov 2020 21:56:24 +0100 wenzelm added document antiquotation @{tool};
Fri, 27 Nov 2020 23:51:37 +0100 wenzelm merged
Fri, 27 Nov 2020 23:47:06 +0100 wenzelm more flexible syntax for theory load commands via Isabelle/Scala;
Fri, 27 Nov 2020 06:48:35 +0000 haftmann refined syntax for bundle mixins for locale and class specifications
Thu, 26 Nov 2020 17:23:33 +0100 wenzelm clarified options: batch-build has pide_reports disabled by default (requires significant resources);
Sun, 22 Nov 2020 13:11:40 +0100 wenzelm updated to cvc4-1.8;
Sat, 21 Nov 2020 19:48:05 +0100 wenzelm tuned NEWS;
Sat, 21 Nov 2020 18:16:25 +0100 wenzelm more NEWS;
Sat, 21 Nov 2020 17:58:00 +0100 wenzelm NEWS;
Sun, 15 Nov 2020 07:17:06 +0000 haftmann bundles for reflected term syntax
Sat, 14 Nov 2020 12:55:05 +0100 wenzelm official support for document theories from other sessions;
Thu, 12 Nov 2020 09:06:44 +0100 haftmann bundled syntax for state monad combinators
Wed, 11 Nov 2020 21:00:14 +0100 wenzelm build documents in Isabelle/Scala, based on generated tex files as session exports;
Sat, 07 Nov 2020 16:49:51 +0100 wenzelm clarified output of "isabelle process";
Wed, 04 Nov 2020 07:39:17 +0000 haftmann NEWS and CONTRIBUTORS
Fri, 30 Oct 2020 22:56:15 +0100 wenzelm Isabelle/Phabricator supports Ubuntu 20.04 LTS;
Thu, 29 Oct 2020 16:07:41 +0100 desharna Added smt (verit) to Sledgehammer's proof preplay.
Thu, 29 Oct 2020 18:23:28 +0000 haftmann unified Local_Theory.init with Generic_Target.init
Thu, 29 Oct 2020 10:03:03 +0000 haftmann moved most material from session HOL-Word to Word_Lib in the AFP
Tue, 27 Oct 2020 22:34:37 +0100 wenzelm clarified signature: overloaded "+" for Path.append;
Mon, 26 Oct 2020 21:35:39 +0100 wenzelm NEWS;
Thu, 15 Oct 2020 13:24:16 +0200 wenzelm proper Isabelle component settings: prefer standard terminology "ISABELLE_VERIT", avoid conflict of "VERIT_VERSION" with processing of implicit options by veriT;
Tue, 13 Oct 2020 20:28:43 +0200 wenzelm merged
Tue, 13 Oct 2020 16:32:48 +0200 wenzelm tuned;
Tue, 13 Oct 2020 16:45:38 +0200 Mathias Fleury reconstruction of veriT proofs in NEWS
Mon, 12 Oct 2020 18:59:44 +0200 Mathias Fleury add reconstruction for the SMT solver veriT
Mon, 12 Oct 2020 17:42:15 +0200 wenzelm NEWS;
Mon, 12 Oct 2020 07:25:38 +0000 haftmann replaced combinators by more conventional nesting pattern
Mon, 12 Oct 2020 07:25:38 +0000 haftmann consolidated names and operations
Wed, 07 Oct 2020 10:39:14 +0200 haftmann consolidated for the sake of documentation
Tue, 29 Sep 2020 13:19:34 +0200 wenzelm allow Scala function execution on separate thread: better reactivity, but potential overloading of the JVM;
Mon, 28 Sep 2020 13:53:50 +0200 wenzelm clarified "isabelle logo", after discontinuation of DVI output (see 564012e31db1);
Sun, 27 Sep 2020 17:02:59 +0200 wenzelm ISABELLE_PDFLATEX is now lualatex;
Sat, 26 Sep 2020 14:29:46 +0200 wenzelm discontinued obsolete DVI document format and related settings/tools;
Fri, 25 Sep 2020 15:43:53 +0200 wenzelm clarified defaults for nitpick;
Fri, 25 Sep 2020 05:26:09 +0000 haftmann factored out typedef material
Wed, 23 Sep 2020 11:14:38 +0000 haftmann more thorough treatment of division, particularly signed division on int and word
Thu, 17 Sep 2020 13:55:21 +0200 haftmann typo
Thu, 17 Sep 2020 12:06:38 +0200 haftmann NEWS and CONTRIBUTORS
Thu, 10 Sep 2020 21:07:58 +0200 wenzelm more uniform JVM vs. ML status widget;
Tue, 08 Sep 2020 21:14:42 +0200 wenzelm update to official jedit-5.6.0;
Mon, 31 Aug 2020 22:05:05 +0200 wenzelm proper use of SELECT_GOAL to confine distinct_subgoals_tac to original goal range (amending 366d39e95d3c);
Tue, 25 Aug 2020 15:14:46 +0200 wenzelm NEWS;
Mon, 17 Aug 2020 16:26:58 +0200 wenzelm allow user-defined server commands via isabelle_scala_service;
Mon, 17 Aug 2020 13:16:42 +0200 wenzelm more systematic support for special directories;
Thu, 13 Aug 2020 15:52:40 +0200 wenzelm more documentation;
Fri, 07 Aug 2020 23:01:28 +0200 wenzelm NEWS;
Thu, 06 Aug 2020 22:43:40 +0200 wenzelm discontinued old batch-build functionality;
Wed, 05 Aug 2020 19:06:39 +0200 haftmann separation of reversed bit lists from other material
Tue, 04 Aug 2020 09:33:05 +0000 haftmann uniform mask operation
Sat, 01 Aug 2020 17:43:30 +0000 haftmann more consequent transferability
Fri, 24 Jul 2020 16:45:20 +0200 wenzelm tuned;
Mon, 20 Jul 2020 23:45:29 +0200 wenzelm subtle change of Theory_Data extend/merge semantics due to Theory.join_theory;
Thu, 16 Jul 2020 04:52:25 +0000 haftmann yet another alias
Mon, 13 Jul 2020 15:23:32 +0000 haftmann concatentation of bit values
Sat, 11 Jul 2020 06:21:04 +0000 haftmann signed_take_bit
Thu, 09 Jul 2020 11:39:16 +0200 desharna Update Metis to 2.4
Mon, 06 Jul 2020 16:52:48 +0200 blanchet removed 'freeze_problem_consts' hack in TPTP tools, which wasn't compatible with post-2016 reforms to local theories
Mon, 06 Jul 2020 10:47:30 +0000 haftmann separation of traditional bit operations
Thu, 02 Jul 2020 12:10:58 +0000 haftmann extraction of equations x = t from premises beneath meta-all
Thu, 02 Jul 2020 08:49:03 +0000 haftmann removed superfluous dependency
Wed, 01 Jul 2020 17:32:11 +0000 haftmann factored out ancient numeral representation
Wed, 01 Jul 2020 17:32:11 +0000 haftmann moved to Word_Lib
Sun, 21 Jun 2020 11:12:19 +0200 wenzelm clarified NEWS;
Sat, 20 Jun 2020 22:35:24 +0200 wenzelm enable pide_session by default (again), with extra JVM heap for AFP tests (see also 86e429abd38d, 026de3424c39);
Fri, 19 Jun 2020 18:44:36 +0200 wenzelm merged
Fri, 19 Jun 2020 18:29:37 +0200 wenzelm back to pide_session=false for now, requires too many JVM resources (reverting 026de3424c39);
Fri, 19 Jun 2020 09:46:47 +0000 haftmann prefer single name
Thu, 18 Jun 2020 09:07:30 +0000 haftmann build bit operations on word on library theory on bit operations
Thu, 18 Jun 2020 09:07:30 +0000 haftmann bit operations as distinctive library theory
Thu, 18 Jun 2020 09:07:29 +0000 haftmann dropped yet another duplicate
Thu, 18 Jun 2020 09:07:29 +0000 haftmann replaced mere alias by input abbreviation
Thu, 18 Jun 2020 09:07:29 +0000 haftmann replaced mere alias by abbreviation
Thu, 18 Jun 2020 09:07:29 +0000 haftmann replaced operation with weak abstraction by input abbreviation
Thu, 18 Jun 2020 09:07:29 +0000 haftmann avoid compound operation
Thu, 18 Jun 2020 09:07:28 +0000 haftmann replaced mere alias by input abbreviation
Wed, 17 Jun 2020 20:42:52 +0200 wenzelm enable pide_session by default;
Wed, 10 Jun 2020 19:59:12 +0200 wenzelm updated to jedit-5.6pre1 (repository version 25349);
Mon, 08 Jun 2020 21:56:06 +0200 wenzelm NEWS;
Mon, 08 Jun 2020 15:09:57 +0200 wenzelm clarified sessions: "Notable Examples in Isabelle/Pure";
Sat, 06 Jun 2020 10:58:13 +0200 haftmann NEWS
Wed, 27 May 2020 16:43:34 +0200 wenzelm tuned;
Wed, 27 May 2020 16:09:25 +0200 wenzelm more NEWS;
Wed, 27 May 2020 14:27:22 +0200 wenzelm check bash functions against Isabelle settings environment;
Wed, 27 May 2020 13:57:13 +0200 wenzelm misc tuning;
Mon, 18 May 2020 12:59:01 +0200 wenzelm follow Phabricator update 2020 Week 19;
Thu, 14 May 2020 10:26:33 +0100 paulson The Uniq quantifier for FOL too
Wed, 13 May 2020 12:55:33 +0200 Manuel Eberl new constant power_int in HOL
Mon, 04 May 2020 17:35:29 +0200 Manuel Eberl New HOL simproc 'datatype_no_proper_subterm'
Tue, 12 May 2020 16:53:02 +0100 paulson Fixes for Sup{} = (0::nat)
Tue, 28 Apr 2020 21:47:22 +0200 wenzelm added "isabelle sessions" tool;
Tue, 21 Apr 2020 07:28:17 +0000 haftmann hooks for foundational terms: protection of foundational terms during simplification
Wed, 15 Apr 2020 14:31:21 +0200 wenzelm merged
Mon, 13 Apr 2020 22:08:14 +0200 wenzelm tuned NEWS; Isabelle2020
Sun, 12 Apr 2020 16:59:49 +0200 wenzelm tuned NEWS;
Thu, 09 Apr 2020 21:50:00 +0200 wenzelm tuned;
Wed, 08 Apr 2020 14:25:28 +0200 wenzelm another isabelle_scala_service;
Wed, 08 Apr 2020 13:14:05 +0200 wenzelm more general support for isabelle_scala_service;
Tue, 07 Apr 2020 22:13:22 +0200 wenzelm NEWS;
Mon, 06 Apr 2020 21:18:16 +0200 wenzelm NEWS;
Thu, 02 Apr 2020 13:04:24 +0200 wenzelm merged
Wed, 25 Mar 2020 17:38:22 +0100 wenzelm more NEWS;
Sat, 21 Mar 2020 22:12:21 +0100 wenzelm merged;
Sat, 21 Mar 2020 21:41:13 +0100 wenzelm more NEWS;
Fri, 20 Mar 2020 22:41:49 +0100 wenzelm more NEWS;
Sun, 15 Mar 2020 13:20:22 +0100 wenzelm back to post-release mode;
Sat, 14 Mar 2020 14:23:52 +0100 wenzelm tuned;
Fri, 13 Mar 2020 23:25:34 +0100 wenzelm proper escape for literal single quotes;
Fri, 13 Mar 2020 16:04:27 +0100 wenzelm allow slightly odd "' " in mixfix as documented (introduced in 55754d6d399c, but broken in be8a8d60d962);
Thu, 12 Mar 2020 23:05:11 +0100 wenzelm updated for release;
Tue, 10 Mar 2020 14:16:19 +0100 Manuel Eberl updated NEWS w.r.t. e0237f2eb49d
Fri, 06 Mar 2020 20:18:21 +0100 wenzelm support Java/VM monitoring via jconsole;
Mon, 02 Mar 2020 13:43:52 +0100 wenzelm more documentation;
Sun, 01 Mar 2020 21:52:21 +0100 wenzelm more Isabelle/jEdit actions;
Sat, 29 Feb 2020 17:16:17 +0100 wenzelm more Isabelle/jEdit actions;
Fri, 28 Feb 2020 22:23:43 +0100 wenzelm NEWS;
Wed, 26 Feb 2020 19:50:04 +0100 wenzelm updated for release;
Wed, 26 Feb 2020 19:26:00 +0100 wenzelm updated for release;
Tue, 25 Feb 2020 18:30:08 +0100 wenzelm update to WebviewPanel API, following initial version by Peter Zeller;
Sun, 16 Feb 2020 20:07:28 +0100 wenzelm NEWS;
Sat, 15 Feb 2020 21:15:03 +0100 wenzelm NEWS;
Tue, 11 Feb 2020 17:03:14 +0100 wenzelm updated for release;
Tue, 11 Feb 2020 15:39:05 +0100 wenzelm updated for release;
Mon, 10 Feb 2020 23:04:45 +0100 wenzelm proper symbols;
Mon, 10 Feb 2020 22:47:43 +0100 wenzelm NEWS;
Mon, 10 Feb 2020 22:40:00 +0100 wenzelm recover from Unicode accident in 4abd07cd034f;
Mon, 10 Feb 2020 22:32:29 +0100 wenzelm NEWS;
Mon, 10 Feb 2020 22:24:01 +0100 wenzelm NEWS;
Mon, 10 Feb 2020 21:59:24 +0100 wenzelm tuned;
Mon, 10 Feb 2020 21:12:52 +0100 wenzelm tuned;
Wed, 15 Jan 2020 15:05:33 +0100 wenzelm added "isabelle scala_project" to support e.g. IntelliJ IDEA;
Mon, 23 Dec 2019 22:30:03 +0100 wenzelm NEWS;
Thu, 19 Dec 2019 17:29:35 +0100 wenzelm NEWS;
Mon, 16 Dec 2019 21:15:12 +0100 wenzelm tuned NEWS;
Mon, 16 Dec 2019 19:58:11 +0100 wenzelm tuned;
Tue, 10 Dec 2019 01:06:39 +0100 traytel NEWS, CONTRIBUTORS, and documentation
Mon, 09 Dec 2019 16:13:36 +0000 paulson Ramsey with multiple colours and arbitrary exponents
Tue, 26 Nov 2019 08:09:44 +0100 ballarin Remove diagnostic command 'print_dependencies'.
Fri, 22 Nov 2019 15:26:08 +0100 haftmann tuned whitespace
Fri, 22 Nov 2019 09:25:01 +0000 haftmann proper prefix syntax
Thu, 21 Nov 2019 15:22:24 +0100 wenzelm tuned;
Thu, 14 Nov 2019 22:37:12 +0100 wenzelm NEWS;
Sun, 27 Oct 2019 20:11:30 -0400 immler NEWS
Sun, 27 Oct 2019 16:47:27 +0100 nipkow NEWS
less more (0) -3000 -1000 -240 tip