aboutsummaryrefslogtreecommitdiff
path: root/src/Util
Commit message (Expand)AuthorAge
...
* Add for-loop combinatorGravatar Jason Gross2017-04-14
* Update display to not line-wrapGravatar Jason Gross2017-04-13
* Add Util.Logic.ImplAndGravatar Jason Gross2017-04-13
* Add lift4_sig_sigGravatar Jason Gross2017-04-13
* Fix missing 'by tac' in rewrite_hypGravatar Jason Gross2017-04-10
* Add dec_of_bool_decGravatar Jason Gross2017-04-10
* Add rewrite_hyp ... by tacGravatar Jason Gross2017-04-10
* Split off ZUtil.Stabilization, finish IsBoundedBy!Gravatar Jason Gross2017-04-09
* Add Z.lt_le_flip_Proper_flip_implGravatar Jason Gross2017-04-09
* Add Z.pow_nonneg to zarithGravatar Jason Gross2017-04-09
* Make replace_with_neg more powerfulGravatar Jason Gross2017-04-09
* Handle more things in Z.peel_leGravatar Jason Gross2017-04-09
* Add Z.peel_leGravatar Jason Gross2017-04-09
* Add Z.log2_up_le_mono to zarithGravatar Jason Gross2017-04-09
* Add Z.max_le_compat Z.min_le_compat to zarithGravatar Jason Gross2017-04-09
* Add lemmas about shift bounds to ZUtilGravatar Jason Gross2017-04-09
* Fix missing unfoldGravatar Jason Gross2017-04-09
* Add sub_le_flip_le_ProperGravatar Jason Gross2017-04-09
* Add Z.shift{l,r}_opp_lGravatar Jason Gross2017-04-08
* Add some le proper flip lemmasGravatar Jason Gross2017-04-08
* Use Z.max 0, not an if statementGravatar Jason Gross2017-04-08
* Add wordToZ_ZToWord_mod_fullGravatar Jason Gross2017-04-08
* Add wordToZ_ZToWord_modGravatar Jason Gross2017-04-08
* Add ZToWord_wordToZ_ZToWord_smallGravatar Jason Gross2017-04-08
* Make dlet-moving on sigma goals use changeGravatar Jason Gross2017-04-07
* Merge branch 'rename-everything'. Closes #14.Gravatar Andres Erbsen2017-04-06
|\
| * rename-everythingGravatar Andres Erbsen2017-04-06
* | Faster clear_all tacticGravatar Jason Gross2017-04-06
| * start removing BaseSystemGravatar Andres Erbsen2017-04-06
| * do not use VerdiTactics in files we plan to keepGravatar Andres Erbsen2017-04-06
|/
* Export ClearAll in TacticsGravatar Jason Gross2017-04-06
* More vigorous clearing in unify_transformed_rhs_abstract_tacGravatar Jason Gross2017-04-06
* Add clear_allGravatar Jason Gross2017-04-06
* make elliptic curve proofs faster and split them into filesGravatar Andres Erbsen2017-04-05
* Don't clutter up typeclass log with cidtacGravatar Jason Gross2017-04-05
* Fix transparent assert by to respect namesGravatar Jason Gross2017-04-05
* Add TransparentAssertGravatar Jason Gross2017-04-05
* Remove bad [Local]Gravatar Jason Gross2017-04-05
* Actually add ChangeInAllGravatar Jason Gross2017-04-05
* Add Tactics.ChangeInAllGravatar Jason Gross2017-04-05
* Fix bug in change_with_curriedGravatar Jason Gross2017-04-05
* When currying, change with curried form in *Gravatar Jason Gross2017-04-05
* Add Tactics.MoveLetInGravatar Jason Gross2017-04-05
* Add Tactics.PrintContextGravatar Jason Gross2017-04-04
* Add [Proof using] to most proofsGravatar Jason Gross2017-04-04
* Move sigma MapProjections to a separate fileGravatar Jason Gross2017-04-04
* Add Tuple.map_ProperGravatar Jason Gross2017-04-03
* More fine-grained tactic importsGravatar Jason Gross2017-04-03
* Split off liftn_sig, add lift{3,4}_sigGravatar Jason Gross2017-04-03
* Fix parsing issueGravatar Jason Gross2017-04-03
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-06 19:05:15 +0000