equal
deleted
inserted
replaced
1 |
1 |
2 (* legacy ML bindings *) |
2 (* legacy ML bindings *) |
3 |
3 |
4 val beta_sscase = thm "beta_sscase"; |
4 val beta_sscase = thm "beta_sscase"; |
|
5 val compact_sinl = thm "compact_sinl"; |
|
6 val compact_sinr = thm "compact_sinr"; |
5 val cont_Iwhen1 = thm "cont_Iwhen1"; |
7 val cont_Iwhen1 = thm "cont_Iwhen1"; |
6 val cont_Iwhen2 = thm "cont_Iwhen2"; |
8 val cont_Iwhen2 = thm "cont_Iwhen2"; |
7 val cont_Iwhen3 = thm "cont_Iwhen3"; |
9 val cont_Iwhen3 = thm "cont_Iwhen3"; |
8 val Exh_Ssum = thm "Exh_Ssum"; |
10 val Exh_Ssum = thm "Exh_Ssum"; |
9 val Iwhen1 = thm "Iwhen1"; |
11 val Iwhen1 = thm "Iwhen1"; |