1 theory QuotTest

     1 theory QuotTest

     2 imports QuotMain

     2 imports QuotMain

     3 begin

     3 begin

     4 

     5 

     5 section {* various tests for quotient types*}

     6 section {* various tests for quotient types*}

     6 datatype trm =

     7 datatype trm =

     7   var  "nat"

     8   var  "nat"

     8 | app  "trm" "trm"

     9 | app  "trm" "trm"