equal
deleted
inserted
replaced
|
1 (* Title: quotient_tacs.thy |
|
2 Author: Cezary Kaliszyk and Christian Urban |
|
3 |
|
4 Tactics for solving goal arising from lifting |
|
5 theorems to quotient types. |
|
6 *) |
|
7 |
1 signature QUOTIENT_TACS = |
8 signature QUOTIENT_TACS = |
2 sig |
9 sig |
3 val regularize_tac: Proof.context -> int -> tactic |
10 val regularize_tac: Proof.context -> int -> tactic |
4 val injection_tac: Proof.context -> int -> tactic |
11 val injection_tac: Proof.context -> int -> tactic |
5 val all_injection_tac: Proof.context -> int -> tactic |
12 val all_injection_tac: Proof.context -> int -> tactic |