equal
deleted
inserted
replaced
8 sig |
8 sig |
9 exception QUOT_THM of typ * typ * Pretty.T |
9 exception QUOT_THM of typ * typ * Pretty.T |
10 exception PARAM_QUOT_THM of typ * Pretty.T |
10 exception PARAM_QUOT_THM of typ * Pretty.T |
11 exception MERGE_TRANSFER_REL of Pretty.T |
11 exception MERGE_TRANSFER_REL of Pretty.T |
12 exception CHECK_RTY of typ * typ |
12 exception CHECK_RTY of typ * typ |
|
13 |
|
14 val instantiate_rtys: Proof.context -> typ * typ -> typ * typ |
13 |
15 |
14 val prove_quot_thm: Proof.context -> typ * typ -> thm |
16 val prove_quot_thm: Proof.context -> typ * typ -> thm |
15 |
17 |
16 val abs_fun: Proof.context -> typ * typ -> term |
18 val abs_fun: Proof.context -> typ * typ -> term |
17 |
19 |