equal
deleted
inserted
replaced
4 val eq_sprod = thm "eq_sprod"; |
4 val eq_sprod = thm "eq_sprod"; |
5 val Exh_Sprod2 = thm "Exh_Sprod2"; (* *) |
5 val Exh_Sprod2 = thm "Exh_Sprod2"; (* *) |
6 val inst_sprod_pcpo2 = thm "inst_sprod_pcpo2"; (* *) |
6 val inst_sprod_pcpo2 = thm "inst_sprod_pcpo2"; (* *) |
7 val less_sprod_def = thm "less_Sprod_def"; |
7 val less_sprod_def = thm "less_Sprod_def"; |
8 val less_sprod = thm "less_sprod"; |
8 val less_sprod = thm "less_sprod"; |
9 val Rep_Sprod_spair = thm "Rep_Sprod_Spair"; |
9 val Rep_Sprod_spair = thm "Rep_Sprod_spair"; |
10 val sfst_defined_iff = thm "sfst_defined_iff"; |
10 val sfst_defined_iff = thm "sfst_defined_iff"; |
11 val sfst_defined = thm "sfst_defined"; |
11 val sfst_defined = thm "sfst_defined"; |
12 val sfst_def = thm "sfst_def"; |
12 val sfst_def = thm "sfst_def"; |
13 val sfst_spair = thm "sfst_spair"; |
13 val sfst_spair = thm "sfst_spair"; |
14 val sfst_strict = thm "sfst_strict"; |
14 val sfst_strict = thm "sfst_strict"; |