134 

   134 

   135 end

   135 end

   136 

   136 

   137 

   137 

   138 section {* type definition for the quotient type *}

   138 section {* type definition for the quotient type *}

   139 

   141 

   140 use "quotient.ML"

   142 use "quotient.ML"

   141 

   143 

   142 declare [[map list = (map, LIST_REL)]]

   144 declare [[map list = (map, LIST_REL)]]

   143 declare [[map * = (prod_fun, prod_rel)]]

   145 declare [[map * = (prod_fun, prod_rel)]]