Structure ind_types


Source File Identifier index Theory binding index

signature ind_types =
sig
 include Abbrev
 type constructor  = string * hol_type list
 type tyspec       = hol_type * constructor list

 val define_type  : tyspec list -> {induction:thm, recursion:thm}

end


Source File Identifier index Theory binding index

HOL 4, Kananaskis-14