equal
deleted
inserted
replaced
3 |
3 |
4 val Iwhen_def = thm "Iwhen_def"; |
4 val Iwhen_def = thm "Iwhen_def"; |
5 val Iwhen1 = thm "Iwhen1"; |
5 val Iwhen1 = thm "Iwhen1"; |
6 val Iwhen2 = thm "Iwhen2"; |
6 val Iwhen2 = thm "Iwhen2"; |
7 val Iwhen3 = thm "Iwhen3"; |
7 val Iwhen3 = thm "Iwhen3"; |
8 val less_ssum_def = thm "less_ssum_def"; |
8 val less_ssum_def = thm "less_Ssum_def"; |
9 val sinl_def = thm "sinl_def"; |
9 val sinl_def = thm "sinl_def"; |
10 val sinr_def = thm "sinr_def"; |
10 val sinr_def = thm "sinr_def"; |
11 val sscase_def = thm "sscase_def"; |
11 val sscase_def = thm "sscase_def"; |
12 val cont_Iwhen1 = thm "cont_Iwhen1"; |
12 val cont_Iwhen1 = thm "cont_Iwhen1"; |
13 val cont_Iwhen2 = thm "cont_Iwhen2"; |
13 val cont_Iwhen2 = thm "cont_Iwhen2"; |