Structure rich_listSimps


Source File Identifier index Theory binding index

signature rich_listSimps =
sig
   val add_rich_list_compset : computeLib.compset -> unit
   val RICH_LIST_ss : simpLib.ssfrag
end


Source File Identifier index Theory binding index

HOL 4, Kananaskis-14