diff -r 77506496e6fd -r cd3fa86be45f Quot/quotient_tacs.ML
--- a/Quot/quotient_tacs.ML	Tue Jan 05 18:10:20 2010 +0100
+++ b/Quot/quotient_tacs.ML	Wed Jan 06 08:24:37 2010 +0100
@@ -1,11 +1,13 @@
 signature QUOTIENT_TACS =
 sig
     val regularize_tac: Proof.context -> int -> tactic
+    val injection_tac: Proof.context -> int -> tactic
     val all_injection_tac: Proof.context -> int -> tactic
     val clean_tac: Proof.context -> int -> tactic
     val procedure_tac: Proof.context -> thm -> int -> tactic
     val lift_tac: Proof.context -> thm -> int -> tactic
     val quotient_tac: Proof.context -> int -> tactic
+    val quot_true_tac: Proof.context -> (term -> term) -> int -> tactic
 end;
 
 structure Quotient_Tacs: QUOTIENT_TACS =
@@ -637,4 +639,4 @@
       (all_injection_tac ctxt, msg2),
       (clean_tac ctxt, msg3)]
 
-end; (* structure *)
\ No newline at end of file
+end; (* structure *)