aboutsummaryrefslogtreecommitdiff
path: root/src/Util/ZUtil.v
Commit message (Expand)AuthorAge
...
* Add Z.pow_le_mono_{r,l} to zarithGravatar Jason Gross2016-10-06
* Add a lemma to Ztestbit about large indicesGravatar Jason Gross2016-10-06
* More zsimplify lemmasGravatar Jason Gross2016-10-04
* Add Zplus_minus to zsimplifyGravatar Jason Gross2016-10-04
* Weaken hyps of zutil lemmaGravatar Jason Gross2016-10-04
* Add a variant of add_shift_modGravatar Jason Gross2016-10-04
* Add ZUtil lemmaGravatar Jason Gross2016-10-04
* Add ZUtil lemmaGravatar Jason Gross2016-10-04
* Add Zmult_lt_compat_r to zarithGravatar Jason Gross2016-10-04
* Prevent infinite loops by not dealing with 0 mod _Gravatar Jason Gross2016-10-04
* Handle 0 mod _ in push_ZmodGravatar Jason Gross2016-10-04
* Handle ?x mod ?x in push_ZmodGravatar Jason Gross2016-10-04
* Z.ltb_to_lt now also handles eqbGravatar Jason Gross2016-10-04
* Reorganization, moving of lemmas to correct files, and 8.4 compatibilityGravatar jadep2016-09-21
* More 8.4 compatibilityGravatar jadep2016-09-14
* Moved lemmas to ZUtilGravatar jadep2016-09-13
* Work around bug #5073 (lia)Gravatar Jason Gross2016-09-07
* More zarithGravatar Jason Gross2016-08-24
* Fewer side-conditions on zsimplifyGravatar Jason Gross2016-08-24
* Fix a Hint Resolve typoGravatar Jason Gross2016-08-23
* More ZUtilGravatar Jason Gross2016-08-23
* More ZUtilGravatar Jason Gross2016-08-23
* Add Z.rewrite_mod_smallGravatar Jason Gross2016-08-19
* More powerful Z.div_mod_to_quot_remGravatar Jason Gross2016-08-19
* More ZUtilGravatar Jason Gross2016-08-18
* Add ZUtilGravatar Jason Gross2016-08-18
* Add a ZUtil hintGravatar Jason Gross2016-08-18
* Add some ZUtil lemmas and hintsGravatar Jason Gross2016-08-18
* Add versions of ZUtil lemmas without nonzero assumptionsGravatar Jason Gross2016-08-18
* Add Z.opp_involutive to Zshift_to_powGravatar Jason Gross2016-08-18
* Add a ZUtil hintGravatar Jason Gross2016-08-17
* Add Z.div_mod_to_quot_remGravatar Jason Gross2016-08-17
* Add [Z.linear_solve_for], [Z.linear_substitute]Gravatar Jason Gross2016-08-17
* More zsimplifyGravatar Jason Gross2016-08-16
* Add a faster zsimplify databaseGravatar Jason Gross2016-08-16
* Merge of conversion development branch with masterGravatar jadep2016-08-16
|\
| * Moved Z lemmas useful for conversion proofs (mostly about bitwise operations)...Gravatar jadep2016-08-16
* | More shift lemmasGravatar Jason Gross2016-08-16
* | More shift logicGravatar Jason Gross2016-08-16
* | More ZUtilGravatar Jason Gross2016-08-16
* | More ZUtil simplificationGravatar Jason Gross2016-08-16
* | Add zutil for div lemmaGravatar Jason Gross2016-08-15
* | Support shiftl in Zshift_to_powGravatar Jason Gross2016-08-15
* | Work around bug #5019 (loopy [zify])Gravatar Jason Gross2016-08-15
* | More ZUtilGravatar Jason Gross2016-08-15
* | Add Z.shift{r,l} databasesGravatar Jason Gross2016-08-15
* | Add upper_bound_uniformGravatar Jason Gross2016-08-12
* | More ZUtilGravatar Jason Gross2016-08-12
* | More ZUtilGravatar Jason Gross2016-08-11
* | Add ZUtilGravatar Jason Gross2016-08-11
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-08 11:19:58 +0000