changeset 952 | 9c3b3eaecaff |
parent 918 | 7be9b054f672 |
child 1101 | 5eb84b817855 |
--- a/Quot/quotient_typ.ML Wed Jan 27 08:20:31 2010 +0100 +++ b/Quot/quotient_typ.ML Wed Jan 27 08:41:42 2010 +0100 @@ -1,3 +1,10 @@ +(* Title: quotient_typ.thy + Author: Cezary Kaliszyk and Christian Urban + + Definition of a quotient type. + +*) + signature QUOTIENT_TYPE = sig val quotient_type: ((string list * binding * mixfix) * (typ * term)) list