2011-11-4: Update by Ondrej Kuncar
- Changes in the monolithic version of formalization:
- Added formalization of deletion
- The rest (namely formalization of insertion) was rewritten to Isar => speedup
- bal_l and bal_r were replaced by more convenient mkt_bal_l and mkt_bal_r functions
- insrt renamed to insert
2006-05-25: Update by Tobias Nipkow
- Did AVL trees properly, with height information in each node.
- Completely revised code and proofs
- Two developments, a monolithic and an incremental one.
- Got rid of the "extended tree type"by Brucker et al
because it stored the wrong information (bal!) and nothing useful
was proved about it.
2004-06-09: Update by Achim Brucker, Burkhart Wolff and Jan Smaus
- parameterized the tree definitions
- added a "efficient" variant of is-in (is_in_eff)
- some proofs about is_ord and is_in_eff
- a extended tree type that stores balancing information in its node and some proofs about it
2004-03-19: First submission
Messung V0.5 in Prozent
¤ Dauer der Verarbeitung: 0.9 Sekunden
(vorverarbeitet am 2026-06-10)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.
