src/HOL/Rings.thy
Sat, 19 Oct 2019 09:15:37 +0000 haftmann generalized
Wed, 09 Oct 2019 14:51:54 +0000 haftmann dedicated fact collections for algebraic simplification rules potentially splitting goals
Fri, 14 Jun 2019 08:34:28 +0000 haftmann official fact collection sign_simps
Tue, 16 Apr 2019 19:50:21 +0000 haftmann removed unused fact collections
Sat, 13 Apr 2019 08:43:33 +0000 haftmann backed out a93e6472ac9c, which does not bring anything substantial: division_ring is not commutative in multiplication but semidom_divide is
Sat, 13 Apr 2019 08:11:48 +0000 haftmann tuned
Sat, 13 Apr 2019 08:11:47 +0000 haftmann more document structure
Sat, 13 Apr 2019 08:11:46 +0000 haftmann tuned
Tue, 09 Apr 2019 16:59:00 +0000 haftmann common type class for distributive division
Mon, 14 Jan 2019 18:35:03 +0000 haftmann tuned proofs
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;
Wed, 23 May 2018 07:13:11 +0000 haftmann grouped material on numeral division
Tue, 22 May 2018 18:14:29 +0000 haftmann automatic classical rule to derive a dvd b from b mod a = 0
Tue, 22 May 2018 18:14:29 +0000 haftmann consider dvdE for automated classical proving
less more (0) -100 -15 tip