src/HOL/Divides.thy
21 months ago ago removed some non-essential rules
21 months ago ago removed some lemma duplicates
23 months ago ago eliminiated superfluous class semiring_bits
23 months ago ago abstract algebraic bit operations
2017-12-19 ago isabelle update_cartouches -c -t;
2017-12-02 ago more simplification rules
2017-11-26 ago more symbols;
2017-11-23 ago new simp rule
2017-10-20 ago added lemmas and tuned proofs
2017-10-09 ago tuned proofs
2017-10-08 ago euclidean rings need no normalization
2017-10-08 ago more fundamental definition of div and mod on int
2017-10-08 ago one uniform type class for parity structures
2017-10-08 ago generalized some rules
2017-10-08 ago generalized simproc
2017-10-08 ago elementary definition of division on natural numbers
2017-10-08 ago abolished (semi)ring_div in favour of euclidean_(semi)ring_cancel
2017-10-08 ago avoid fact name clashes
2017-10-08 ago spelling and tuned whitespace
2017-09-08 ago speed up proofs slightly
2017-04-23 ago more lemmas
2017-01-09 ago slightly generalized type class hierarchy concerning unit factors, to allow for lean polynomial normalization
2017-01-04 ago moved euclidean ring to HOL
2016-12-31 ago more elementary rules about div / mod on int
2016-12-22 ago more uniform div/mod relations
2016-12-20 ago emphasize dedicated rewrite rules for congruences
2016-12-17 ago reoriented congruence rules in non-explosive direction
2016-12-17 ago more fine-grained type class hierarchy for div and mod
2016-10-16 ago clarified prover-specific rules
2016-10-16 ago eliminated irregular aliasses
2016-10-16 ago clarified theorem names
2016-10-16 ago eliminated irregular aliasses
2016-10-16 ago more standardized theorem names for facts involving the div and mod identity
2016-10-16 ago more standardized names
2016-10-16 ago de-orphanized declaration
2016-10-12 ago separate type class for arbitrary quotient and remainder partitions
2016-10-03 ago more lemmas
2016-09-26 ago syntactic type class for operation mod named after mod;
2016-09-26 ago more lemmas
2016-09-11 ago tuned proofs;
2016-07-14 ago Tuned looping simp rules in semiring_div
2016-07-09 ago more lemmas to emphasize {0::nat..(<)n} as canonical representation of intervals on nat
2016-06-16 ago Various additions to polynomials, FPSs, Gamma function
2016-05-25 ago isabelle update_cartouches -c -t;
2016-04-25 ago eliminated old 'def';
2016-03-12 ago model characters directly as range 0..255
2016-02-23 ago more canonical names
2015-12-28 ago prefer symbols for "abs";
2015-12-07 ago isabelle update_cartouches -c -t;
2015-11-13 ago Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
2015-10-17 ago qualify some names stemming from internal bootstrap constructions
2015-09-27 ago monomorphization of divmod wrt. code generation avoids costly dictionary unpacking at runtime
2015-09-19 ago eliminated suspicious unicode;
2015-09-01 ago eliminated \<Colon>;
2015-08-13 ago qualified adjust_*
2015-08-08 ago direct bootstrap of integer division from natural division
2015-08-06 ago slight cleanup of lemmas
2015-07-18 ago isabelle update_cartouches;
2015-07-08 ago tuned facts
2015-07-08 ago moved normalization and unit_factor into Main HOL corpus