15 val sinl_strict = thm "sinl_strict"; |
15 val sinl_strict = thm "sinl_strict"; |
16 val sinr_strict = thm "sinr_strict"; |
16 val sinr_strict = thm "sinr_strict"; |
17 val noteq_sinlsinr = thm "noteq_sinlsinr"; |
17 val noteq_sinlsinr = thm "noteq_sinlsinr"; |
18 val sinl_inject = thm "sinl_inject"; |
18 val sinl_inject = thm "sinl_inject"; |
19 val sinr_inject = thm "sinr_inject"; |
19 val sinr_inject = thm "sinr_inject"; |
|
20 val sinl_eq = thm "sinl_eq"; |
|
21 val sinr_eq = thm "sinr_eq"; |
20 val sinl_defined = thm "sinl_defined"; |
22 val sinl_defined = thm "sinl_defined"; |
21 val sinr_defined = thm "sinr_defined"; |
23 val sinr_defined = thm "sinr_defined"; |
22 val Exh_Ssum1 = thm "Exh_Ssum1"; |
24 val Exh_Ssum1 = thm "Exh_Ssum1"; |
23 val ssumE = thm "ssumE"; |
25 val ssumE = thm "ssumE"; |
24 val ssumE2 = thm "ssumE2"; |
26 val ssumE2 = thm "ssumE2"; |
|
27 val sinl_less = thm "sinl_less"; |
|
28 val sinr_less = thm "sinr_less"; |
|
29 val sinl_less_sinr = thm "sinl_less_sinr"; |
|
30 val sinr_less_sinl = thm "sinr_less_sinl"; |
25 val sscase1 = thm "sscase1"; |
31 val sscase1 = thm "sscase1"; |
26 val sscase2 = thm "sscase2"; |
32 val sscase2 = thm "sscase2"; |
27 val sscase3 = thm "sscase3"; |
33 val sscase3 = thm "sscase3"; |
28 val less_ssum4a = thm "less_ssum4a"; |
|
29 val less_ssum4b = thm "less_ssum4b"; |
|
30 val less_ssum4c = thm "less_ssum4c"; |
|
31 val less_ssum4d = thm "less_ssum4d"; |
|
32 val sscase4 = thm "sscase4"; |
34 val sscase4 = thm "sscase4"; |
33 val Ssum_rews = [sinl_strict, sinr_strict, sinl_defined, sinr_defined, |
35 val Ssum_rews = [sinl_strict, sinr_strict, sinl_defined, sinr_defined, |
34 sscase1, sscase2, sscase3]; |
36 sscase1, sscase2, sscase3]; |