equal
deleted
inserted
replaced
19 val sprodE = thm "sprodE"; |
19 val sprodE = thm "sprodE"; |
20 val sfst_strict = thm "sfst_strict"; |
20 val sfst_strict = thm "sfst_strict"; |
21 val ssnd_strict = thm "ssnd_strict"; |
21 val ssnd_strict = thm "ssnd_strict"; |
22 val sfst_spair = thm "sfst_spair"; |
22 val sfst_spair = thm "sfst_spair"; |
23 val ssnd_spair = thm "ssnd_spair"; |
23 val ssnd_spair = thm "ssnd_spair"; |
24 val sfstssnd_defined = thm "sfstssnd_defined"; |
24 val sfst_defined = thm "sfst_defined"; |
|
25 val ssnd_defined = thm "ssnd_defined"; |
25 val surjective_pairing_Sprod2 = thm "surjective_pairing_Sprod2"; |
26 val surjective_pairing_Sprod2 = thm "surjective_pairing_Sprod2"; |
26 val less_sprod = thm "less_sprod"; |
27 val less_sprod = thm "less_sprod"; |
27 val spair_less = thm "spair_less"; |
28 val spair_less = thm "spair_less"; |
28 val ssplit1 = thm "ssplit1"; |
29 val ssplit1 = thm "ssplit1"; |
29 val ssplit2 = thm "ssplit2"; |
30 val ssplit2 = thm "ssplit2"; |