theory Set_Toolkit imports"HOL-Library.Multiset""Relation_Lib" begin
text‹ The majority of the Z set toolkit is implemented in the core libraries of HOL. We could
prove all the axioms of ISO 13568 as theorems, but we omit this for now. The main thing we
need is to map between finite sets and the normal set type. ›
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.
