equal
deleted
inserted
replaced
1 signature QUOTIENT_TACS = |
1 signature QUOTIENT_TACS = |
2 sig |
2 sig |
3 val regularize_tac: Proof.context -> int -> tactic |
3 val regularize_tac: Proof.context -> int -> tactic |
|
4 val injection_tac: Proof.context -> int -> tactic |
4 val all_injection_tac: Proof.context -> int -> tactic |
5 val all_injection_tac: Proof.context -> int -> tactic |
5 val clean_tac: Proof.context -> int -> tactic |
6 val clean_tac: Proof.context -> int -> tactic |
6 val procedure_tac: Proof.context -> thm -> int -> tactic |
7 val procedure_tac: Proof.context -> thm -> int -> tactic |
7 val lift_tac: Proof.context -> thm -> int -> tactic |
8 val lift_tac: Proof.context -> thm -> int -> tactic |
8 val quotient_tac: Proof.context -> int -> tactic |
9 val quotient_tac: Proof.context -> int -> tactic |
|
10 val quot_true_tac: Proof.context -> (term -> term) -> int -> tactic |
9 end; |
11 end; |
10 |
12 |
11 structure Quotient_Tacs: QUOTIENT_TACS = |
13 structure Quotient_Tacs: QUOTIENT_TACS = |
12 struct |
14 struct |
13 |
15 |