--- a/quotient.ML	Sun Oct 18 00:52:10 2009 +0200
+++ b/quotient.ML	Sun Oct 18 08:44:16 2009 +0200
@@ -2,6 +2,8 @@
 sig
   val mk_quotient_type: ((binding * mixfix) * (typ * term)) list -> Proof.context -> Proof.state
   val mk_quotient_type_cmd: (((bstring * mixfix) * string) * string) list -> Proof.context -> Proof.state
+  val define: binding * mixfix * term -> local_theory -> (term * thm) * local_theory
+  val note: binding * thm -> local_theory -> thm * local_theory
 end;
 
 structure Quotient: QUOTIENT =