(* Author: Andreas Lochbihler, ETH Zurich Author: Joshua Schneider, ETH Zurich *) theory Operation_Examples imports Composition Fixpoints Subtypes Quotient_Preservation begin end