1 theory QuotMain

     1 theory QuotMain

     2 imports QuotScript QuotList Prove

     2 imports QuotScript QuotList Prove

     4 begin

     5 begin

     5 

     6 

     6 ML {* Attrib.empty_binding *}

     7 ML {* Attrib.empty_binding *}

     7 

     8 

     8 locale QUOT_TYPE =

     9 locale QUOT_TYPE =

   137 end

   138 end

   138 

   139 

   139 

   140 

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

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

   141 

   142 

   142 use "quotient.ML"

   144 use "quotient.ML"

   143 

   145 

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

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

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

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

   146 declare [[map "fun" = (fun_map, FUN_REL)]]

   148 declare [[map "fun" = (fun_map, FUN_REL)]]