Changelog » History » Version 1
Ilya Shchepetkov, 07/30/2021 03:22 PM
| 1 | 1 | Ilya Shchepetkov | h1. Changelog |
|---|---|---|---|
| 2 | |||
| 3 | h2. 2021-07-30 |
||
| 4 | |||
| 5 | Версия Rodin 3.6.0.202107301121-8d606770d, версия SMT Solvers 1.4.0.f64afaac |
||
| 6 | |||
| 7 | * [smt] Добавлена "аксиома пустого множества":https://ru.wikipedia.org/wiki/Аксиома_пустого_множества |
||
| 8 | * [smt] В тактику @Default Auto tactic with SMT@ добавлен запуск SMT решателей до выполнения тактики @Lasso@ |
||
| 9 | * [rodin] Добавлена тактика @Disjunction to Implication in Hypotheses (Simplify)@ |
||
| 10 | * [rodin] Добавлена тактика @Disjunction to Implication in Goal (Simplify)@ |
||
| 11 | * [rodin] Добавлена тактика @Set Equality Rewrites in Hypotheses (Simplify)@ |
||
| 12 | * [rodin] Добавлена тактика @Set Equality Rewrites in Goal (Simplify)@ |
||
| 13 | * [rodin] Добавлена тактика @Disjunctions in Hypotheses (Split)@ |
||
| 14 | * [rodin] Добавлена тактика @Implications in Hypotheses (Split)@ |
||
| 15 | * [rodin] Добавлена тактика @Relation Overriding in Hypotheses (Split)@ |
||
| 16 | * [rodin] Добавлена тактика @Relation Overriding in Goal (Split)@ |
||
| 17 | |||
| 18 | h2. 2021-07-09 |
||
| 19 | |||
| 20 | Версия Rodin 3.6.0.202107091733-b8b571eb7, версия SMT Solvers 1.4.0.8eee0d1f |
||
| 21 | |||
| 22 | * [rodin] Распараллелен запуск действий @Retry Auto Provers@, @Recalculate Auto Status@ и @Proof Replay on Undischarged POs@ |
||
| 23 | * [rodin] На вкладке @Auto/Post Tactic@ настроек добавлено меню интерактивных тактик, заточенных под интерактивное доказательство |
||
| 24 | * [smt] Добавлена интерактивная тактика @Default Interactive tactic with SMT@ |
||
| 25 | * [smt] Добавлена тактика @All enabled SMT configurations in parallel@ |
||
| 26 | * [rodin] Добавлена тактика-комбинатор @First Successful@, которая позволяет запускать несколько других тактик параллельно |