2 imports QuotScript QuotList Prove

     2 imports QuotScript QuotList Prove

     3 uses ("quotient_info.ML") 

     3 uses ("quotient_info.ML") 

     4      ("quotient.ML")

     4      ("quotient.ML")

     5      ("quotient_def.ML")

     5      ("quotient_def.ML")

     6 begin

     6 begin

     7 

     8 

     8 locale QUOT_TYPE =

     9 locale QUOT_TYPE =

     9   fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"

    10   fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"

    10   and   Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"

    11   and   Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"

    11   and   Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)"

    12   and   Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)"