Fri, 19 Jul 2019 12:57:14 +0100 paulson More results about measure and integration theory
Thu, 18 Jul 2019 15:40:15 +0100 paulson More analysis / measure theory material
Thu, 18 Jul 2019 14:08:44 +0100 paulson merged
Thu, 18 Jul 2019 14:08:28 +0100 paulson more new material about analysis
Thu, 18 Jul 2019 12:06:42 +0200 nipkow added forgotten declaration provided by Florian Haftmann
Wed, 17 Jul 2019 22:24:20 +0200 wenzelm merged;
Wed, 17 Jul 2019 21:56:32 +0200 wenzelm updated to jedit_build-20190717: support more brackets;
Wed, 17 Jul 2019 21:32:03 +0200 wenzelm updated to isabelle_fonts-20190717;
Wed, 17 Jul 2019 17:12:57 +0200 wenzelm redundant;
Wed, 17 Jul 2019 17:03:50 +0200 wenzelm tuned;
Wed, 17 Jul 2019 16:10:05 +0200 wenzelm added \<llangle>, \<rrangle>;
Wed, 17 Jul 2019 11:18:39 +0200 wenzelm tuned doc isar-ref;
Wed, 17 Jul 2019 11:09:43 +0200 wenzelm added \<bbar>;
Wed, 17 Jul 2019 09:40:43 +0200 wenzelm added \<sqdot>;
Wed, 17 Jul 2019 16:32:06 +0100 paulson fixed renaming issues
Wed, 17 Jul 2019 14:02:50 +0100 paulson merged
Wed, 17 Jul 2019 14:02:42 +0100 paulson a few new lemmas and a bit of tidying
Tue, 16 Jul 2019 15:39:32 +0200 wenzelm support for a soft-type system within the Isabelle logical framework;
Thu, 11 Jul 2019 18:37:52 +0200 nipkow tuned
Thu, 04 Jul 2019 14:20:47 +0200 wenzelm proper theory naming after join (reset due to merge_data);
Thu, 04 Jul 2019 12:31:24 +0200 wenzelm support join of anonymous theory nodes, e.g. relevant for parallel theory construction;
Thu, 04 Jul 2019 11:26:00 +0200 wenzelm clarified history stage: allow independent updates that are merged later;
Mon, 24 Jun 2019 16:26:25 +0200 wenzelm support abstract syntax for proof terms (see src/Pure/Proofs/proof_syntax.ML);
Sun, 23 Jun 2019 13:42:16 +0000 haftmann proper quasi-total merge
Sat, 22 Jun 2019 16:23:25 +0200 haftmann made LaTeX happy
Sat, 22 Jun 2019 07:18:55 +0000 haftmann streamlined setup for linear algebra, particularly removed redundant rule declarations
Sat, 22 Jun 2019 06:25:34 +0000 haftmann tuned
Fri, 21 Jun 2019 18:55:00 +0000 haftmann tuned
Sun, 16 Jun 2019 16:40:57 +0000 haftmann even more appropriate fact name
Sun, 16 Jun 2019 16:40:57 +0000 haftmann more correct indicator
Fri, 14 Jun 2019 12:29:50 +0200 haftmann make latex happy
Fri, 14 Jun 2019 08:34:28 +0000 haftmann moved some theorems into HOL main corpus
Fri, 14 Jun 2019 08:34:28 +0000 haftmann misc tuning and modernization
Fri, 14 Jun 2019 08:34:28 +0000 haftmann more theorems for proof of concept for word type
Fri, 14 Jun 2019 08:34:28 +0000 haftmann official fact collection sign_simps
Fri, 14 Jun 2019 08:34:28 +0000 haftmann tuned proofs
Fri, 14 Jun 2019 08:34:27 +0000 haftmann avoid pseudo-collection to be used in generated proofs
Fri, 14 Jun 2019 08:34:27 +0000 haftmann moved comment to approproiate place
Fri, 14 Jun 2019 08:34:27 +0000 haftmann removed outcommented example which seems not to work as advertized
Fri, 14 Jun 2019 08:34:27 +0000 haftmann clear separation of types for bits (False / True) and Z2 (0 / 1)
Fri, 14 Jun 2019 08:34:27 +0000 haftmann generalized type classes for parity to cover word types also, which contain zero divisors
Fri, 14 Jun 2019 08:34:27 +0000 haftmann slightly more specialized name for type class
Fri, 14 Jun 2019 08:34:27 +0000 haftmann dropped weaker legacy alias
Fri, 14 Jun 2019 08:34:27 +0000 haftmann slightly more stringent ordering of theorems
Fri, 14 Jun 2019 08:34:27 +0000 haftmann removed relics of ASCII syntax for indexed big operators
Fri, 14 Jun 2019 08:34:27 +0000 haftmann dropped former legacy input abbreviations
Fri, 14 Jun 2019 08:34:27 +0000 haftmann using (*)-syntax for partially applied infix is fine, contrary to ancient op-syntax
Fri, 14 Jun 2019 08:34:27 +0000 haftmann prefer fixed simpset for proof procedure
Fri, 14 Jun 2019 08:34:27 +0000 haftmann tuned file system structure
Fri, 14 Jun 2019 08:34:27 +0000 haftmann avoid spammed sledgehammer proofs
Tue, 11 Jun 2019 18:33:27 +0200 nipkow added lemmas
Sun, 09 Jun 2019 22:23:41 +0200 wenzelm proper URL;
Sun, 09 Jun 2019 22:22:36 +0200 wenzelm merged;
Sun, 09 Jun 2019 20:24:16 +0200 wenzelm Added tag Isabelle2019 for changeset 83774d669b51
Fri, 07 Jun 2019 11:08:29 +0200 blanchet handle timeouts gracefully in 'smt' proof method (patch due to Mathias Fleury)
Tue, 04 Jun 2019 20:49:33 +0200 wenzelm tuned;
Tue, 04 Jun 2019 20:01:02 +0200 wenzelm tuned;
Tue, 04 Jun 2019 19:51:45 +0200 wenzelm backout 34bc296374ee -- affects the raw_induct rule, e.g. relevant for AFP/Imperative_Insertion_Sort;
Tue, 04 Jun 2019 17:04:25 +0200 wenzelm unused;
Tue, 04 Jun 2019 17:04:18 +0200 wenzelm tuned messages;
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 tip