changeset 789 | 8237786171f1 |
parent 776 | d1064fa29424 |
child 799 | 0755f8fd56b3 |
--- a/Quot/quotient_def.ML Fri Dec 25 00:17:55 2009 +0100 +++ b/Quot/quotient_def.ML Fri Dec 25 00:58:06 2009 +0100 @@ -3,6 +3,7 @@ sig val quotient_def: mixfix -> Attrib.binding -> term -> term -> local_theory -> (term * thm) * local_theory + val quotdef_cmd: (Attrib.binding * string) * (mixfix * string) -> local_theory -> local_theory end;