2 (* legacy ML bindings *) |
2 (* legacy ML bindings *) |
3 |
3 |
4 val Isinl_def = thm "Isinl_def"; |
4 val Isinl_def = thm "Isinl_def"; |
5 val Isinr_def = thm "Isinr_def"; |
5 val Isinr_def = thm "Isinr_def"; |
6 val Iwhen_def = thm "Iwhen_def"; |
6 val Iwhen_def = thm "Iwhen_def"; |
7 val SsumIl = thm "SsumIl"; |
|
8 val SsumIr = thm "SsumIr"; |
|
9 val inj_on_Abs_Ssum = thm "inj_on_Abs_Ssum"; |
7 val inj_on_Abs_Ssum = thm "inj_on_Abs_Ssum"; |
10 val strict_SinlSinr_Rep = thm "strict_SinlSinr_Rep"; |
|
11 val strict_IsinlIsinr = thm "strict_IsinlIsinr"; |
8 val strict_IsinlIsinr = thm "strict_IsinlIsinr"; |
12 val noteq_SinlSinr_Rep = thm "noteq_SinlSinr_Rep"; |
|
13 val noteq_IsinlIsinr = thm "noteq_IsinlIsinr"; |
9 val noteq_IsinlIsinr = thm "noteq_IsinlIsinr"; |
14 val inject_Sinl_Rep1 = thm "inject_Sinl_Rep1"; |
|
15 val inject_Sinr_Rep1 = thm "inject_Sinr_Rep1"; |
|
16 val inject_Sinl_Rep2 = thm "inject_Sinl_Rep2"; |
|
17 val inject_Sinr_Rep2 = thm "inject_Sinr_Rep2"; |
|
18 val inject_Sinl_Rep = thm "inject_Sinl_Rep"; |
|
19 val inject_Sinr_Rep = thm "inject_Sinr_Rep"; |
|
20 val inject_Isinl = thm "inject_Isinl"; |
10 val inject_Isinl = thm "inject_Isinl"; |
21 val inject_Isinr = thm "inject_Isinr"; |
11 val inject_Isinr = thm "inject_Isinr"; |
22 val inject_Isinl_rev = thm "inject_Isinl_rev"; |
12 val inject_Isinl_rev = thm "inject_Isinl_rev"; |
23 val inject_Isinr_rev = thm "inject_Isinr_rev"; |
13 val inject_Isinr_rev = thm "inject_Isinr_rev"; |
24 val Exh_Ssum = thm "Exh_Ssum"; |
14 val Exh_Ssum = thm "Exh_Ssum"; |