src/HOL/Divides.thy
Fri, 14 Jun 2019 08:34:27 +0000 haftmann slightly more specialized name for type class
Mon, 04 Feb 2019 12:16:03 +0100 Manuel Eberl More material for HOL-Number_Theory: ord, Carmichael's function, primitive roots
Sat, 19 Jan 2019 20:40:17 +0000 haftmann algebraized more material from theory Divides
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);
Mon, 16 Jul 2018 23:33:28 +0100 paulson de-applying and simplifying proofs
Sat, 14 Jul 2018 22:32:15 +0100 paulson de-applying
Fri, 13 Jul 2018 17:18:07 +0100 paulson de-applying
Thu, 24 May 2018 09:18:29 +0200 haftmann avoid overaggressive classical rule
Wed, 23 May 2018 07:13:11 +0000 haftmann grouped material on numeral division
Sat, 12 May 2018 22:20:46 +0200 haftmann removed some non-essential rules
Sun, 06 May 2018 18:20:25 +0000 haftmann removed some lemma duplicates
Mon, 12 Mar 2018 08:25:35 +0000 haftmann eliminiated superfluous class semiring_bits
Sat, 10 Mar 2018 19:36:59 +0000 haftmann abstract algebraic bit operations
Tue, 19 Dec 2017 13:58:12 +0100 wenzelm isabelle update_cartouches -c -t;
Sat, 02 Dec 2017 16:50:53 +0000 haftmann more simplification rules
Sun, 26 Nov 2017 21:08:32 +0100 wenzelm more symbols;
Thu, 23 Nov 2017 13:00:00 +0000 haftmann new simp rule
Fri, 20 Oct 2017 07:46:10 +0200 haftmann added lemmas and tuned proofs
Mon, 09 Oct 2017 19:10:48 +0200 haftmann tuned proofs
Sun, 08 Oct 2017 22:28:22 +0200 haftmann euclidean rings need no normalization
Sun, 08 Oct 2017 22:28:22 +0200 haftmann more fundamental definition of div and mod on int
Sun, 08 Oct 2017 22:28:22 +0200 haftmann one uniform type class for parity structures
Sun, 08 Oct 2017 22:28:22 +0200 haftmann generalized some rules
Sun, 08 Oct 2017 22:28:21 +0200 haftmann generalized simproc
Sun, 08 Oct 2017 22:28:21 +0200 haftmann elementary definition of division on natural numbers
Sun, 08 Oct 2017 22:28:21 +0200 haftmann abolished (semi)ring_div in favour of euclidean_(semi)ring_cancel
Sun, 08 Oct 2017 22:28:20 +0200 haftmann avoid fact name clashes
Sun, 08 Oct 2017 22:28:19 +0200 haftmann spelling and tuned whitespace
Fri, 08 Sep 2017 00:02:33 +0200 blanchet speed up proofs slightly
Sun, 23 Apr 2017 14:53:35 +0200 haftmann more lemmas
Mon, 09 Jan 2017 18:53:06 +0100 haftmann slightly generalized type class hierarchy concerning unit factors, to allow for lean polynomial normalization
Wed, 04 Jan 2017 21:28:29 +0100 haftmann moved euclidean ring to HOL
Sat, 31 Dec 2016 08:12:31 +0100 haftmann more elementary rules about div / mod on int
Thu, 22 Dec 2016 10:42:08 +0100 haftmann more uniform div/mod relations
Tue, 20 Dec 2016 15:39:13 +0100 haftmann emphasize dedicated rewrite rules for congruences
Sat, 17 Dec 2016 15:22:14 +0100 haftmann reoriented congruence rules in non-explosive direction
Sat, 17 Dec 2016 15:22:14 +0100 haftmann more fine-grained type class hierarchy for div and mod
Sun, 16 Oct 2016 13:47:37 +0200 haftmann clarified prover-specific rules
Sun, 16 Oct 2016 09:31:06 +0200 haftmann eliminated irregular aliasses
Sun, 16 Oct 2016 09:31:05 +0200 haftmann clarified theorem names
Sun, 16 Oct 2016 09:31:05 +0200 haftmann eliminated irregular aliasses
Sun, 16 Oct 2016 09:31:05 +0200 haftmann more standardized theorem names for facts involving the div and mod identity
Sun, 16 Oct 2016 09:31:04 +0200 haftmann more standardized names
Sun, 16 Oct 2016 09:31:03 +0200 haftmann de-orphanized declaration
Wed, 12 Oct 2016 20:38:47 +0200 haftmann separate type class for arbitrary quotient and remainder partitions
Mon, 03 Oct 2016 14:34:32 +0200 haftmann more lemmas
Mon, 26 Sep 2016 07:56:54 +0200 haftmann syntactic type class for operation mod named after mod;
Mon, 26 Sep 2016 07:56:54 +0200 haftmann more lemmas
Sun, 11 Sep 2016 00:14:44 +0200 wenzelm tuned proofs;
Thu, 14 Jul 2016 14:43:09 +0200 eberlm Tuned looping simp rules in semiring_div
Sat, 09 Jul 2016 13:26:16 +0200 haftmann more lemmas to emphasize {0::nat..(<)n} as canonical representation of intervals on nat
Thu, 16 Jun 2016 17:57:09 +0200 eberlm Various additions to polynomials, FPSs, Gamma function
Wed, 25 May 2016 11:49:40 +0200 wenzelm isabelle update_cartouches -c -t;
Mon, 25 Apr 2016 16:09:26 +0200 wenzelm eliminated old 'def';
Sat, 12 Mar 2016 22:04:52 +0100 haftmann model characters directly as range 0..255
Tue, 23 Feb 2016 16:25:08 +0100 nipkow more canonical names
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;
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.
less more (0) -100 -60 tip