changeset 329 | 5d06e1dba69a |
parent 321 | f46dc0ca08c3 |
child 331 | 345c422b1cb5 |
--- a/quotient.ML Sat Nov 21 14:45:25 2009 +0100 +++ b/quotient.ML Sat Nov 21 23:23:01 2009 +0100 @@ -39,8 +39,8 @@ end -(* definition of the quotient type *) -(***********************************) +(* definition of quotient types *) +(********************************) (* constructs the term lambda (c::rty => bool). EX (x::rty). c = rel x *) fun typedef_term rel rty lthy =