Structure UniversalType


Source File Identifier index Theory binding index

signature UniversalType =
sig
  type t

  val embed: unit -> ('a -> t) * (t -> 'a option)
end


Source File Identifier index Theory binding index

HOL 4, Kananaskis-13