isabelle: File revisions

Mercurial Mercurial > repos > isabelle / file revisions

src/HOL/Euclidean_Division.thy

2021-10-26	haftmann	more generic bit/word lemmas for distribution	file \| diff \| annotate
2021-06-16	haftmann	more lemmas	file \| diff \| annotate
2021-04-11	haftmann	collected combinatorial material	file \| diff \| annotate
2021-04-06	haftmann	new lemmas	file \| diff \| annotate
2020-08-21	haftmann	more lemmas	file \| diff \| annotate
2020-03-08	haftmann	more frugal simp rules for bit operations; more pervasive use of bit selector	file \| diff \| annotate
2020-02-01	haftmann	more specific class assumptions	file \| diff \| annotate
2020-02-01	haftmann	more theorems	file \| diff \| annotate
2020-01-26	haftmann	more theorems	file \| diff \| annotate
2019-11-23	haftmann	tuned theory structure	file \| diff \| annotate
2019-04-13	haftmann	backed out a93e6472ac9c, which does not bring anything substantial: division_ring is not commutative in multiplication but semidom_divide is	file \| diff \| annotate
2019-04-09	haftmann	common type class for distributive division	file \| diff \| annotate
2019-01-19	haftmann	algebraized more material from theory Divides	file \| diff \| annotate
2019-01-04	wenzelm	isabelle update -u control_cartouches;	file \| diff \| annotate
2018-06-28	wenzelm	avoid pending shyps in global theory facts;	file \| diff \| annotate
2017-12-02	haftmann	more simplification rules	file \| diff \| annotate
2017-11-23	haftmann	generalized more lemmas	file \| diff \| annotate
2017-11-23	haftmann	new simp rule	file \| diff \| annotate
2017-11-11	haftmann	dedicated definition for coprimality	file \| diff \| annotate
2017-10-20	haftmann	added lemmas and tuned proofs	file \| diff \| annotate
2017-10-09	haftmann	canonical multiplicative euclidean size	file \| diff \| annotate
2017-10-09	haftmann	clarified parity	file \| diff \| annotate
2017-10-09	haftmann	clarified uniqueness criterion for euclidean rings	file \| diff \| annotate
2017-10-09	haftmann	tuned proofs	file \| diff \| annotate
2017-10-08	haftmann	euclidean rings need no normalization	file \| diff \| annotate
2017-10-08	haftmann	more fundamental definition of div and mod on int	file \| diff \| annotate
2017-10-08	haftmann	generalized some rules	file \| diff \| annotate
2017-10-08	haftmann	avoid variant of mk_sum	file \| diff \| annotate
2017-10-08	haftmann	generalized simproc	file \| diff \| annotate
2017-10-08	haftmann	elementary definition of division on natural numbers	file \| diff \| annotate
2017-10-08	haftmann	tuned structure	file \| diff \| annotate
2017-10-08	haftmann	abolished (semi)ring_div in favour of euclidean_(semi)ring_cancel	file \| diff \| annotate
2017-10-08	haftmann	fundamental property of division by units	file \| diff \| annotate
2017-01-04	haftmann	moved euclidean ring to HOL	file \| diff \| annotate

less more (0) tip

isabelle

RSS Atom