epfl-lara / lisa

Proof assistant based on first-order logic and set theory
Apache License 2.0
33 stars 18 forks source link

Set2 #126

Closed SimonGuilloud closed 1 year ago

SimonGuilloud commented 1 year ago

Reduced size of two proofs on pairs that were necessary for the later development

Improvements and bug correction on axioms

Some corrections for DSL and overload resolution

Remove OutputManager as input from some places where it is not needed

Delete old "tactics" files

Introduce new traits for proof tactics to help dsl

Move Peano files and old SetTheory+Mapping files to tests, rename SetTheory2 in SetTheory