Expand description
This module defines a fold function for finite sets and proves a number of associated lemmas.
The module was ported (with some modifications) from Isabelle/HOL’s finite set theory in:
HOL/Finite_Set.thy
That file contains the following author list:
(* Title: HOL/Finite_Set.thy Author: Tobias Nipkow Author: Lawrence C Paulson Author: Markus Wenzel Author: Jeremy Avigad Author: Andrei Popescu *)
The file is distributed under a 3-clause BSD license as indicated in the file COPYRIGHT
in Isabelle’s root directory, which also carries the following copyright notice:
Copyright (c) 1986-2024, University of Cambridge, Technische Universitaet Muenchen, and contributors.