src/HOL/HOL.thy
Thu, 02 Jul 2020 12:10:58 +0000 haftmann extraction of equations x = t from premises beneath meta-all
Fri, 19 Jun 2020 09:46:47 +0000 haftmann prefer single name
Thu, 04 Jun 2020 15:30:22 +0000 haftmann more simp rules
Sat, 30 May 2020 08:50:18 +0000 haftmann install simproc but deactivate by default
Sun, 24 May 2020 19:57:13 +0000 haftmann better closeup and more consistent terminology
Wed, 13 May 2020 16:35:36 +0200 Manuel Eberl new HOL simproc: eliminate_false_implies
Tue, 12 May 2020 15:11:20 +0100 paulson abbrevs for the Uniq quantifier; trying Sup_nat_def to allow zero (experimentally)
Mon, 11 May 2020 11:15:41 +0100 paulson the Uniq quantifier
Sat, 28 Mar 2020 17:27:01 +0000 paulson structured a lot of ancient, horrible proofs
Tue, 03 Mar 2020 19:26:23 +0000 haftmann tuned
Tue, 15 Oct 2019 13:30:02 +0200 wenzelm tuned signature;
Sun, 13 Oct 2019 16:26:31 +0200 wenzelm clarified sessions/directories;
Sat, 12 Oct 2019 18:41:12 +0200 wenzelm setup preprocessing for HOL proofs;
Sat, 12 Oct 2019 16:46:33 +0200 wenzelm early setup of proof preprocessing;
Wed, 07 Aug 2019 18:23:32 +0200 wenzelm prefer named lemmas -- more compact proofterms;
Tue, 04 Jun 2019 20:49:33 +0200 wenzelm tuned;
Sun, 06 Jan 2019 15:04:34 +0100 wenzelm isabelle update -u path_cartouches;
Sat, 05 Jan 2019 17:24:33 +0100 wenzelm isabelle update -u control_cartouches;
Fri, 04 Jan 2019 23:22:53 +0100 wenzelm isabelle update -u control_cartouches;
Wed, 31 Oct 2018 15:53:32 +0100 wenzelm clarified ML_Context.expression: it is a closed expression, not a let-declaration -- thus source positions are more accurate (amending d8849cfad60f, 162a4c2e97bc);
Wed, 12 Sep 2018 17:12:33 +0100 paulson merged
Tue, 11 Sep 2018 16:21:54 +0100 paulson A few new results, elimination of duplicates and more use of "pairwise"
Wed, 12 Sep 2018 16:12:50 +0200 nipkow tuned "=" syntax declarations; made "~=" uniformly "infix"
Wed, 02 May 2018 13:49:38 +0200 immler added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
Sun, 25 Feb 2018 12:54:55 +0000 paulson new material on matrices, etc., and consolidating duplicate results about of_nat
Mon, 19 Feb 2018 16:44:45 +0000 paulson lots of new material, ultimately related to measure theory
Tue, 16 Jan 2018 09:30:00 +0100 wenzelm standardized towards new-style formal comments: isabelle update_comments;
Thu, 11 Jan 2018 13:48:17 +0100 wenzelm uniform use of Standard ML op-infix -- eliminated warnings;
Wed, 10 Jan 2018 15:25:09 +0100 nipkow ran isabelle update_op on all sources
Fri, 29 Dec 2017 19:17:52 +0100 wenzelm prefer formal citations;
Wed, 06 Dec 2017 20:43:09 +0100 wenzelm prefer control symbol antiquotations;
Sun, 26 Nov 2017 21:08:32 +0100 wenzelm more symbols;
Sun, 22 Oct 2017 09:10:10 +0200 nipkow derived axiom iffI as a lemma (thanks to Alexander Maletzky)
Mon, 09 Oct 2017 19:10:47 +0200 haftmann tuned imports
Sun, 02 Jul 2017 20:13:38 +0200 haftmann proper concept of code declaration wrt. atomicity and Isar declarations
Sat, 17 Jun 2017 15:41:19 +0200 nipkow added simp rules
Sun, 18 Sep 2016 17:59:28 +0200 wenzelm clarified notation: iterated quantifier is negated as one chunk;
Sun, 18 Sep 2016 15:16:42 +0200 wenzelm clarified notation;
Mon, 01 Aug 2016 22:11:29 +0200 wenzelm misc tuning and modernization;
Fri, 29 Jul 2016 09:49:23 +0200 Andreas Lochbihler add lemmas contributed by Peter Gammie
Tue, 12 Apr 2016 14:38:57 +0200 wenzelm Type_Infer.object_logic controls improvement of type inference result;
Fri, 08 Apr 2016 20:15:20 +0200 wenzelm eliminated unused simproc identifier;
Sat, 05 Mar 2016 20:47:31 +0100 wenzelm abbreviations for \<nexists>;
Sat, 05 Mar 2016 19:58:56 +0100 wenzelm old HOL syntax is for input only;
Tue, 23 Feb 2016 16:25:08 +0100 nipkow more canonical names
Tue, 12 Jan 2016 11:49:35 +0100 wenzelm eliminated old defs;
Mon, 28 Dec 2015 21:47:32 +0100 wenzelm former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
Sun, 27 Dec 2015 17:16:21 +0100 wenzelm discontinued ASCII replacement syntax <->;
Tue, 22 Dec 2015 15:39:01 +0100 haftmann stripped some legacy
Mon, 07 Dec 2015 10:38:04 +0100 wenzelm isabelle update_cartouches -c -t;
Fri, 09 Oct 2015 20:26:03 +0200 wenzelm discontinued specific HTML syntax;
Mon, 21 Sep 2015 21:46:14 +0200 wenzelm isabelle update_cartouches;
Mon, 21 Sep 2015 11:31:56 +0200 nipkow Added new simplifier predicate ASSUMPTION
Sun, 13 Sep 2015 22:56:52 +0200 wenzelm tuned proofs -- less legacy;
Wed, 09 Sep 2015 20:57:21 +0200 wenzelm simplified simproc programming interfaces;
Tue, 01 Sep 2015 22:32:58 +0200 wenzelm eliminated \<Colon>;
Sat, 25 Jul 2015 23:41:53 +0200 wenzelm updated to infer_instantiate;
Mon, 20 Jul 2015 11:40:43 +0200 wenzelm proper LaTeX;
Sun, 19 Jul 2015 00:03:10 +0200 wenzelm more symbols;
Sat, 18 Jul 2015 22:58:50 +0200 wenzelm isabelle update_cartouches;
less more (0) -300 -100 -60 tip