(* Title: HOL/Corec_Examples/Tests/Type_Class.thy Author: Andreas Lochbihler, ETH Zuerich Author: Jasmin Blanchette, Inria, LORIA, MPII Copyright 2016 Tests type class instances as friends. *) section ‹Tests Type Class Instances as Friends› theory Type_Class imports "HOL-Library.BNF_Corec" "HOL-Library.Stream" begin instantiation stream :: (plus) plus begin definition plus_stream where "plus_stream s1 s2 = smap (λ(x, y). x + y) (sproduct s1 s2)" instance .. end