All notable changes to this project will be documented in this file.
The format is based on Keep a Changelog, and this project adheres to Semantic Versioning.
- Add scaladocs for (almost) all methods
- Update to use Isabelle 2025
- Remove useless intermediary proofs
- Restore lambdapi output
- Remove old code (in particular src/rootfile.scala and src/dkcheck.scala)
- Update to Isabelle 2024 (Melanie Taprogge)
- Turn equational axioms defining type classes into definitions (Frédéric Blanqui)
- Add export to Rocq (Frédéric Blanqui)
- Update to Isabelle 2023 and improvements (Akihisa Yamada)
Update to Isabelle 2022 (Frédéric Blanqui, Jérémy Dubut, Akihisa Yamada)
Improvements (Frédéric Blanqui, Jérémy Dubut, Akihisa Yamada)
Modular export of all Isabelle/HOL standard library (Jérémy Dubut, Akihisa Yamada and Frédéric Blanqui)
- patch Isabelle/HOL standard library
- introduce command isabelle dedukti_generate
- creates a ROOT file with a session for each theory
- fix Dedukti and Lambapi outputs
- make Dedukti output modular
- Update translator to 2021-03 lambdapi syntax
- Escaping :ddd identifiers
- Add infix symbols, unicode glyphs
- Add notation-less lambdapi output
- Include new wrapped operator syntax
- No more useless disambiguation, better detection of can be implicit arg
- Fix for bound variables
- eta-contract
- Add possibility of skipping eta flag (not final) and add documentation
- Describe project structure
- Enable Github Actions
- Fix proofboxes in wrong files (doesn't scale well)
- Dedukti output fix
- Add patch to remove enum's proofs
- Add patch to remove String's proofs
- Some more comments
- Reach the limits of eta_expansion
- Only write optional arguments if no other argument follows
- Update to Isabelle-2021-1-RC1 by Makarius Wenzel
Improvements (Makarius Wenzel)
Use Isabelle 2020 (Makarius Wenzel)
Improvements (Makarius Wenzel)
Add Lambdapi output (Michael Färber)
Improvements (Makarius Wenzel)
First version (Makarius Wenzel)