Theory CU

(* Countable version of UFOL structures: *)
theory CU
imports U
begin

locale Struct = U.Struct wtFsym wtPsym arOf parOf D intF intP
for wtFsym and wtPsym
and arOf :: "'fsym  nat"
and parOf :: "'psym  nat"
and D :: "univ  bool"
and intF :: "'fsym  univ list  univ"
and intP :: "'psym  univ list  bool"

locale Model = U.Model wtFsym wtPsym arOf parOf Φ D intF intP
for wtFsym and wtPsym
and arOf :: "'fsym  nat"
and parOf :: "'psym  nat"
and Φ
and D :: "univ  bool"
and intF :: "'fsym  univ list  univ"
and intP :: "'psym  univ list  bool"


end