Commit message (Expand) | Author | Age | |
---|---|---|---|
* | More 8.4 compatibility | 2016-09-14 | |
* | Moved lemmas to ZUtil | 2016-09-13 | |
* | Work around bug #5073 (lia) | 2016-09-07 | |
* | More zarith | 2016-08-24 | |
* | Fewer side-conditions on zsimplify | 2016-08-24 | |
* | Fix a Hint Resolve typo | 2016-08-23 | |
* | More ZUtil | 2016-08-23 | |
* | More ZUtil | 2016-08-23 | |
* | Add Z.rewrite_mod_small | 2016-08-19 | |
* | More powerful Z.div_mod_to_quot_rem | 2016-08-19 | |
* | More ZUtil | 2016-08-18 | |
* | Add ZUtil | 2016-08-18 | |
* | Add a ZUtil hint | 2016-08-18 | |
* | Add some ZUtil lemmas and hints | 2016-08-18 | |
* | Add versions of ZUtil lemmas without nonzero assumptions | 2016-08-18 | |
* | Add Z.opp_involutive to Zshift_to_pow | 2016-08-18 | |
* | Add a ZUtil hint | 2016-08-17 | |
* | Add Z.div_mod_to_quot_rem | 2016-08-17 | |
* | Add [Z.linear_solve_for], [Z.linear_substitute] | 2016-08-17 | |
* | More zsimplify | 2016-08-16 | |
* | Add a faster zsimplify database | 2016-08-16 | |
* | Merge of conversion development branch with master | 2016-08-16 | |
|\ | |||
| * | Moved Z lemmas useful for conversion proofs (mostly about bitwise operations)... | 2016-08-16 | |
* | | More shift lemmas | 2016-08-16 | |
* | | More shift logic | 2016-08-16 | |
* | | More ZUtil | 2016-08-16 | |
* | | More ZUtil simplification | 2016-08-16 | |
* | | Add zutil for div lemma | 2016-08-15 | |
* | | Support shiftl in Zshift_to_pow | 2016-08-15 | |
* | | Work around bug #5019 (loopy [zify]) | 2016-08-15 | |
* | | More ZUtil | 2016-08-15 | |
* | | Add Z.shift{r,l} databases | 2016-08-15 | |
* | | Add upper_bound_uniform | 2016-08-12 | |
* | | More ZUtil | 2016-08-12 | |
* | | More ZUtil | 2016-08-11 | |
* | | Add ZUtil | 2016-08-11 | |
* | | Add {pull,push}_Zof_nat | 2016-08-11 | |
|/ | |||
* | More ZUtil | 2016-08-09 | |
* | More ZUtil | 2016-08-09 | |
* | More ZUtil | 2016-08-09 | |
* | zsimplify: Better support for existentials | 2016-08-08 | |
* | More zarith hints | 2016-08-08 | |
* | Add ZUtil lemmas | 2016-08-08 | |
* | Handle [_ mod 0] in pull_Zmod | 2016-08-05 | |
* | Add Z.mod_mod case to pull_Zmod | 2016-08-05 | |
* | Handle [((-_) mod n) mod n] in {push,pull}_Zmod | 2016-08-04 | |
* | More zsimplify | 2016-08-03 | |
* | Add some autogenerated zsimplify lemmas | 2016-08-03 | |
* | Better Zmod manipulation | 2016-08-03 | |
* | Weaken some ZUtil assumptions | 2016-08-03 |