Changelog¶

2021-07-30¶

Версия Rodin 3.6.0.202107301121-8d606770d, версия SMT Solvers 1.4.0.f64afaac

• [smt] Добавлена аксиома пустого множества
• [smt] В тактику Default Auto tactic with SMT добавлен запуск SMT решателей до выполнения тактики Lasso
• [rodin] Добавлена тактика Disjunction to Implication in Hypotheses (Simplify)
• [rodin] Добавлена тактика Disjunction to Implication in Goal (Simplify)
• [rodin] Добавлена тактика Set Equality Rewrites in Hypotheses (Simplify)
• [rodin] Добавлена тактика Set Equality Rewrites in Goal (Simplify)
• [rodin] Добавлена тактика Disjunctions in Hypotheses (Split)
• [rodin] Добавлена тактика Implications in Hypotheses (Split)
• [rodin] Добавлена тактика Relation Overriding in Hypotheses (Split)
• [rodin] Добавлена тактика Relation Overriding in Goal (Split)

2021-07-09¶

Версия Rodin 3.6.0.202107091733-b8b571eb7, версия SMT Solvers 1.4.0.8eee0d1f

• [rodin] Распараллелен запуск действий Retry Auto Provers, Recalculate Auto Status и Proof Replay on Undischarged POs
• [rodin] На вкладке Auto/Post Tactic настроек добавлено меню интерактивных тактик, заточенных под интерактивное доказательство
• [smt] Добавлена интерактивная тактика Default Interactive tactic with SMT
• [smt] Добавлена тактика All enabled SMT configurations in parallel
• [rodin] Добавлена тактика-комбинатор First Successful, которая позволяет запускать несколько других тактик параллельно