Theory Shows_Literal_List

theory Shows_Literal_List
imports Shows_Literal
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