theory SetOfSet imports "~~/src/HOL/Library/Executable_Set"
begin

definition
  inter_partition :: "'a set set \<Rightarrow> 'a set set \<Rightarrow> 'a set set" where
  "inter_partition P Q = ((\<lambda> (a,b). a \<inter> b) ` (P \<times> Q))"

  (* missing in Executable_Set *)
setup {*
  Code.add_signature_cmd ("exTimes", "'a set \<Rightarrow> 'b set \<Rightarrow> ('a * 'b) set")
*}

setup {*
  Code.add_signature_cmd ("inter_partition", "'a set set \<Rightarrow> 'a set set \<Rightarrow> 'a set set")
*}

export_code inter_partition in OCaml module_name SetOfSet file "set_of_set.ml"


end