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