src/HOL/Int.thy
Mon, 04 Feb 2019 17:19:04 +0100 Manuel Eberl Formal Laurent series and overhaul of Formal power series (due to Jeremy Sylvestre)
Mon, 21 Jan 2019 14:44:23 +0000 paulson new material about summations and powers, along with some tweaks
Sun, 06 Jan 2019 15:04:34 +0100 wenzelm isabelle update -u path_cartouches;
Fri, 04 Jan 2019 23:22:53 +0100 wenzelm isabelle update -u control_cartouches;
Thu, 25 Oct 2018 09:48:02 +0000 haftmann more and generalized lemmas
Sat, 04 Aug 2018 01:03:39 +0200 eberlm Small lemmas about analysis
Mon, 09 Apr 2018 15:20:11 +0100 paulson Syntax for the special cases Min(A`I) and Max (A`I)
Wed, 10 Jan 2018 15:25:09 +0100 nipkow ran isabelle update_op on all sources
Sat, 02 Dec 2017 16:50:53 +0000 haftmann more simplification rules
Sat, 02 Dec 2017 16:50:53 +0000 haftmann cleaned up and tuned
Tue, 24 Oct 2017 18:48:21 +0200 immler generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
Fri, 20 Oct 2017 07:46:10 +0200 haftmann added lemmas and tuned proofs
Mon, 09 Oct 2017 19:10:47 +0200 haftmann tuned imports
Sun, 08 Oct 2017 22:28:22 +0200 haftmann more fundamental definition of div and mod on int
Thu, 08 Jun 2017 23:37:01 +0200 boehmes replace non-arithmetic terms by fresh variables before replaying linear-arithmetic proofs: avoid failed proof replays due to an overambitious simpset which may cause proof replay to diverge from the pre-computed proof trace
Tue, 07 Feb 2017 22:15:04 +0100 haftmann dropped superfluous preprocessing rule
Mon, 09 Jan 2017 18:53:20 +0100 haftmann moved some lemmas to appropriate places
Tue, 03 Jan 2017 16:48:49 +0000 paulson A few new lemmas and needed adaptations
Fri, 30 Dec 2016 18:02:27 +0100 haftmann complete set of cases rules for integers known to be (non-)positive/negative;
Mon, 17 Oct 2016 17:33:07 +0200 nipkow setprod -> prod
Mon, 17 Oct 2016 11:46:22 +0200 nipkow setsum -> sum
Mon, 03 Oct 2016 14:34:32 +0200 haftmann more lemmas
Wed, 10 Aug 2016 22:03:58 +0200 wenzelm misc tuning and modernization;
Wed, 10 Aug 2016 09:33:54 +0200 nipkow "split add" -> "split"
Fri, 22 Jul 2016 08:02:37 +0200 wenzelm tuned proofs -- avoid improper use of "this";
Tue, 23 Feb 2016 16:25:08 +0100 nipkow more canonical names
Wed, 17 Feb 2016 21:51:57 +0100 haftmann dropped various legacy fact bindings
Wed, 17 Feb 2016 21:51:57 +0100 haftmann generalized some lemmas;
Mon, 11 Jan 2016 16:38:39 +0100 eberlm Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
Mon, 28 Dec 2015 01:26:34 +0100 wenzelm prefer symbols for "abs";
Mon, 07 Dec 2015 10:38:04 +0100 wenzelm isabelle update_cartouches -c -t;
Mon, 23 Nov 2015 16:57:54 +0000 paulson New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
Tue, 17 Nov 2015 12:32:08 +0000 paulson Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
Fri, 13 Nov 2015 12:27:13 +0000 paulson Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
Tue, 10 Nov 2015 14:18:41 +0000 paulson Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
Mon, 02 Nov 2015 16:17:09 +0100 eberlm Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
Mon, 02 Nov 2015 11:56:28 +0100 eberlm Rounding function, uniform limits, cotangent, binomial identities
Thu, 29 Oct 2015 15:40:52 +0100 eberlm added many small lemmas about setsum/setprod/powr/...
Tue, 22 Sep 2015 16:55:07 +0100 paulson New lemmas
Mon, 21 Sep 2015 19:52:13 +0100 paulson new lemmas and movement of lemmas into place
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>;
Mon, 31 Aug 2015 21:28:08 +0200 wenzelm prefer symbols;
Sat, 08 Aug 2015 10:51:33 +0200 haftmann direct bootstrap of integer division from natural division
Sat, 18 Jul 2015 22:58:50 +0200 wenzelm isabelle update_cartouches;
Thu, 25 Jun 2015 15:01:42 +0200 haftmann more theorems
Thu, 30 Apr 2015 15:28:01 +0100 paulson tidying some messy proofs
Tue, 10 Mar 2015 15:20:40 +0000 paulson Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
Thu, 05 Mar 2015 17:30:29 +0000 paulson The function frac. Various lemmas about limits, series, the exp function, etc.
Wed, 04 Mar 2015 19:53:18 +0100 wenzelm tuned signature -- prefer qualified names;
Wed, 18 Feb 2015 22:46:48 +0100 haftmann eliminated technical fact alias
Sat, 14 Feb 2015 10:24:15 +0100 haftmann dropped redundancy
Thu, 13 Nov 2014 17:19:52 +0100 hoelzl import general theorems from AFP/Markov_Models
Sun, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section;
Sun, 12 Oct 2014 17:05:35 +0200 haftmann some more facts on divisibility
Sun, 12 Oct 2014 17:05:34 +0200 haftmann generalized and consolidated some theorems concerning divisibility
Thu, 02 Oct 2014 11:33:06 +0200 haftmann moved lemmas out of Int.thy which have nothing to do with int
Sat, 05 Jul 2014 11:01:53 +0200 haftmann prefer ac_simps collections over separate name bindings for add and mult
Fri, 04 Jul 2014 20:18:47 +0200 haftmann reduced name variants for assoc and commute on plus and mult
less more (0) -100 -60 tip