equal
deleted
inserted
replaced
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 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"; |
|
18 val sinl_inject = thm "sinl_inject"; |
17 val sinl_inject = thm "sinl_inject"; |
19 val sinr_inject = thm "sinr_inject"; |
18 val sinr_inject = thm "sinr_inject"; |
20 val sinl_eq = thm "sinl_eq"; |
19 val sinl_eq = thm "sinl_eq"; |
21 val sinr_eq = thm "sinr_eq"; |
20 val sinr_eq = thm "sinr_eq"; |
22 val sinl_defined = thm "sinl_defined"; |
21 val sinl_defined = thm "sinl_defined"; |