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"; |
14 val cont_Iwhen3 = thm "cont_Iwhen3"; |
14 val cont_Iwhen3 = thm "cont_Iwhen3"; |
15 val strict_sinl = thm "strict_sinl"; |
15 val sinl_strict = thm "sinl_strict"; |
16 val strict_sinr = thm "strict_sinr"; |
16 val sinr_strict = thm "sinr_strict"; |
17 val noteq_sinlsinr = thm "noteq_sinlsinr"; |
17 val noteq_sinlsinr = thm "noteq_sinlsinr"; |
18 val inject_sinl = thm "inject_sinl"; |
18 val sinl_inject = thm "sinl_inject"; |
19 val inject_sinr = thm "inject_sinr"; |
19 val sinr_inject = thm "sinr_inject"; |
20 val defined_sinl = thm "defined_sinl"; |
20 val sinl_defined = thm "sinl_defined"; |
21 val defined_sinr = thm "defined_sinr"; |
21 val sinr_defined = thm "sinr_defined"; |
22 val Exh_Ssum1 = thm "Exh_Ssum1"; |
22 val Exh_Ssum1 = thm "Exh_Ssum1"; |
23 val ssumE = thm "ssumE"; |
23 val ssumE = thm "ssumE"; |
24 val ssumE2 = thm "ssumE2"; |
24 val ssumE2 = thm "ssumE2"; |
25 val sscase1 = thm "sscase1"; |
25 val sscase1 = thm "sscase1"; |
26 val sscase2 = thm "sscase2"; |
26 val sscase2 = thm "sscase2"; |
28 val less_ssum4a = thm "less_ssum4a"; |
28 val less_ssum4a = thm "less_ssum4a"; |
29 val less_ssum4b = thm "less_ssum4b"; |
29 val less_ssum4b = thm "less_ssum4b"; |
30 val less_ssum4c = thm "less_ssum4c"; |
30 val less_ssum4c = thm "less_ssum4c"; |
31 val less_ssum4d = thm "less_ssum4d"; |
31 val less_ssum4d = thm "less_ssum4d"; |
32 val sscase4 = thm "sscase4"; |
32 val sscase4 = thm "sscase4"; |
33 val Ssum_rews = [strict_sinl, strict_sinr, defined_sinl, defined_sinr, |
33 val Ssum_rews = [sinl_strict, sinr_strict, sinl_defined, sinr_defined, |
34 sscase1, sscase2, sscase3] |
34 sscase1, sscase2, sscase3]; |