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