src/HOL/Euclidean_Division.thy
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;
Thu, 28 Jun 2018 21:05:56 +0200 wenzelm avoid pending shyps in global theory facts;
Sat, 02 Dec 2017 16:50:53 +0000 haftmann more simplification rules
Thu, 23 Nov 2017 17:03:27 +0000 haftmann generalized more lemmas
Thu, 23 Nov 2017 13:00:00 +0000 haftmann new simp rule
Sat, 11 Nov 2017 18:41:08 +0000 haftmann dedicated definition for coprimality
Fri, 20 Oct 2017 07:46:10 +0200 haftmann added lemmas and tuned proofs
Mon, 09 Oct 2017 19:10:52 +0200 haftmann canonical multiplicative euclidean size
Mon, 09 Oct 2017 19:10:51 +0200 haftmann clarified parity
Mon, 09 Oct 2017 19:10:49 +0200 haftmann clarified uniqueness criterion for euclidean rings
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 generalized some rules
Sun, 08 Oct 2017 22:28:22 +0200 haftmann avoid variant of mk_sum
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 tuned structure
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:19 +0200 haftmann fundamental property of division by units
Wed, 04 Jan 2017 21:28:29 +0100 haftmann moved euclidean ring to HOL
less more (0) tip