src/HOL/HOL.thy
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;
Sat, 09 May 2015 12:19:24 +0200 nipkow undid 6d7b7a037e8d because it does not help but slows simplification down by up to 5% (AODV)
Sun, 03 May 2015 15:38:25 +0200 nipkow swap False to the right in assumptions to be eliminated at the right end
Tue, 28 Apr 2015 19:09:28 +0200 nipkow undid 6d7b7a037e8d
Sat, 25 Apr 2015 17:38:22 +0200 nipkow new ==> simp rule
Wed, 22 Apr 2015 12:11:48 +0200 nipkow added simp rules for ==>
Thu, 09 Apr 2015 20:42:32 +0200 wenzelm clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);
Wed, 08 Apr 2015 19:39:08 +0200 wenzelm proper context for Object_Logic operations;
Mon, 06 Apr 2015 23:14:05 +0200 wenzelm local setup of induction tools, with restricted access to auxiliary consts;
Mon, 06 Apr 2015 12:37:21 +0200 wenzelm tuned;
Tue, 31 Mar 2015 17:29:44 +0200 nipkow added lemmas
Mon, 23 Mar 2015 15:08:02 +0100 hoelzl fix parameter order of NO_MATCH
Fri, 06 Mar 2015 23:14:41 +0100 wenzelm clarified context;
Fri, 06 Mar 2015 15:58:56 +0100 wenzelm Thm.cterm_of and Thm.ctyp_of operate on local context;
Wed, 04 Mar 2015 22:05:01 +0100 wenzelm clarified signature;
Wed, 04 Mar 2015 19:53:18 +0100 wenzelm tuned signature -- prefer qualified names;
Wed, 11 Feb 2015 12:01:56 +0000 paulson Merge
Tue, 10 Feb 2015 16:08:11 +0000 paulson New lemmas and a bit of tidying up.
Tue, 10 Feb 2015 16:46:21 +0100 wenzelm misc tuning;
Tue, 10 Feb 2015 14:48:26 +0100 wenzelm proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
Sat, 22 Nov 2014 11:36:00 +0100 wenzelm named_theorems: multiple args;
Mon, 10 Nov 2014 21:49:48 +0100 wenzelm proper context for assume_tac (atac remains as fall-back without context);
Sun, 09 Nov 2014 18:27:43 +0100 wenzelm proper context;
Sun, 09 Nov 2014 17:04:14 +0100 wenzelm proper context for match_tac etc.;
Sun, 09 Nov 2014 14:08:00 +0100 wenzelm proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
Sun, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section;
Thu, 30 Oct 2014 22:45:19 +0100 wenzelm eliminated aliases;
Thu, 30 Oct 2014 09:15:54 +0100 hoelzl disable coercions for NO_MATCH
Wed, 29 Oct 2014 19:01:49 +0100 wenzelm modernized setup;
Fri, 24 Oct 2014 15:07:49 +0200 hoelzl move NO_MATCH simproc from the AFP entry Graph_Theory to HOL
Mon, 13 Oct 2014 18:45:48 +0200 wenzelm Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
Sat, 16 Aug 2014 22:14:57 +0200 wenzelm updated to named_theorems;
Sat, 16 Aug 2014 21:11:08 +0200 wenzelm updated to named_theorems;
Sat, 16 Aug 2014 20:46:59 +0200 wenzelm updated to named_theorems;
Sat, 16 Aug 2014 13:23:50 +0200 wenzelm modernized module name and setup;
Fri, 04 Jul 2014 20:18:47 +0200 haftmann reduced name variants for assoc and commute on plus and mult
Mon, 12 May 2014 17:17:32 +0200 wenzelm tuned signature to make axiomatizations more easy to spot in the source, via "add_axioms" or "axiomatization";
Thu, 03 Apr 2014 10:51:22 +0200 blanchet use same idiom as used for datatype 'size' function to name constants and theorems emerging from various type interpretations -- reduces the chances of name clashes on theory merges
Wed, 26 Feb 2014 11:57:52 +0100 haftmann prefer proof context over background theory
Thu, 20 Feb 2014 20:19:41 +0100 wenzelm modernized tool setup;
Mon, 10 Feb 2014 22:08:18 +0100 wenzelm discontinued axiomatic 'classes', 'classrel', 'arities';
Mon, 10 Feb 2014 21:03:28 +0100 wenzelm more explicit axiomatization;
Sat, 01 Feb 2014 21:09:53 +0100 wenzelm more standard file/module names;
Wed, 01 Jan 2014 01:05:48 +0100 haftmann fundamental treatment of undefined vs. universally partial replaces code_abort
Sat, 14 Dec 2013 17:28:05 +0100 wenzelm proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
Thu, 22 Aug 2013 21:15:43 +0200 haftmann congruence rules for code_simp to mimic typical non-strict behaviour of conj and disj
Sun, 14 Jul 2013 00:08:15 +0200 wenzelm recover static nnf_ss from 6c0de045d127 -- avoid odd runtime warnings due to duplication of not_not;
Sat, 13 Jul 2013 00:50:49 +0200 wenzelm hybrid "auto" tool setup, for TTY (within theory) and PIDE (global print function);
Sun, 23 Jun 2013 21:16:07 +0200 haftmann migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
Sun, 23 Jun 2013 22:31:50 +0200 wenzelm tuned message -- more markup;
Thu, 30 May 2013 12:35:40 +0200 wenzelm standardized aliases;
Sat, 25 May 2013 15:37:53 +0200 wenzelm syntax translations always depend on context;
Sat, 27 Apr 2013 20:50:20 +0200 wenzelm uniform Proof.context for hyp_subst_tac;
Thu, 18 Apr 2013 17:07:01 +0200 wenzelm simplifier uses proper Proof.context instead of historic type simpset;
Wed, 10 Apr 2013 21:20:35 +0200 wenzelm tuned pretty layout: avoid nested Pretty.string_of, which merely happens to work with Isabelle/jEdit since formatting is delegated to Scala side;
Wed, 10 Apr 2013 19:14:47 +0200 wenzelm merged
Wed, 10 Apr 2013 17:17:16 +0200 wenzelm discontinued obsolete ML antiquotation @{claset};
Tue, 22 Jan 2013 14:33:45 +0100 traytel separate data used for case translation from the datatype package
Thu, 28 Feb 2013 16:54:52 +0100 wenzelm just one HOLogic.Trueprop_conv, with regular exception CTERM;
Thu, 28 Feb 2013 13:24:51 +0100 wenzelm marginalized historic strip_tac;
Wed, 06 Feb 2013 17:18:01 +0100 hoelzl check alpha equality after applying beta and eta conversion in let-simproc, otherwise the simplifier may loop
Wed, 05 Dec 2012 11:05:23 +0100 nipkow \<noteq> now has the same associativity as ~= and =
Wed, 12 Sep 2012 22:00:29 +0200 wenzelm eliminated some old material that is unused in the visible universe;
Wed, 22 Aug 2012 22:55:41 +0200 wenzelm prefer ML_file over old uses;
Sat, 11 Aug 2012 22:17:46 +0200 wenzelm faster compilation of ML with antiquotations: static ML_context is bound once in auxiliary structure Isabelle;
Thu, 05 Jul 2012 16:58:03 +0200 wenzelm removed obsolete rev_contrapos (cf. 1d195de59497);
Tue, 05 Jun 2012 07:10:51 +0200 haftmann prefer sys.error over plain error in Scala to avoid deprecation warning
Thu, 19 Apr 2012 19:36:24 +0200 haftmann moved modules with only vague relation to the code generator to theory HOL rather than theory Code_Generator
Fri, 16 Mar 2012 22:31:19 +0100 wenzelm modernized axiomatization;
Thu, 15 Mar 2012 22:08:53 +0100 wenzelm declare command keywords via theory header, including strict checking outside Pure;
Wed, 15 Feb 2012 23:19:30 +0100 wenzelm renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
Wed, 11 Jan 2012 21:04:22 +0100 wenzelm more conventional eval_tac vs. method_setup "eval";
Mon, 09 Jan 2012 18:29:42 +0100 wenzelm prefer antiquotations;
Thu, 05 Jan 2012 18:18:39 +0100 wenzelm improved case syntax: more careful treatment of position constraints, which enables PIDE markup;
Sun, 27 Nov 2011 23:10:19 +0100 wenzelm more antiquotations;
Thu, 24 Nov 2011 21:01:06 +0100 wenzelm modernized some old-style infix operations, which were left over from the time of ML proof scripts;
Sun, 20 Nov 2011 21:07:10 +0100 wenzelm eliminated obsolete "standard";
Fri, 28 Oct 2011 23:41:16 +0200 wenzelm tuned Named_Thms: proper binding;
Fri, 21 Oct 2011 11:17:14 +0200 bulwahn replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
Wed, 19 Oct 2011 08:37:16 +0200 bulwahn removing old code generator setup in the HOL theory
less more (0) -120 tip