theory Shows_Literal_List imports Shows_Literal begin instantiation list :: (showl) showl begin definition showsl_list :: "'a list ⇒ showsl" where "showsl_list (xs :: 'a list) = showl_class.showsl_list xs" definition "showsl_list_list (xs :: 'a list list) = default_showsl_list showsl xs" instance .. end end