Mercurial Mercurial > hg > nominal2 / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Quot/quotient_tacs.ML
changeset 814 cd3fa86be45f
parent 804 ba7e81531c6d
child 826 e3732ed89dfc 
--- 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 *)
nominal2