equal
deleted
inserted
replaced
1461 Thm ("separate_bdv_n", num_str @{thm separate_bdv_n}), |
1461 Thm ("separate_bdv_n", num_str @{thm separate_bdv_n}), |
1462 Thm ("separate_1_bdv", num_str @{thm separate_1_bdv}), |
1462 Thm ("separate_1_bdv", num_str @{thm separate_1_bdv}), |
1463 (*"?bdv / ?b = (1 / ?b) * ?bdv"*) |
1463 (*"?bdv / ?b = (1 / ?b) * ?bdv"*) |
1464 Thm ("separate_1_bdv_n", num_str @{thm separate_1_bdv_n}), |
1464 Thm ("separate_1_bdv_n", num_str @{thm separate_1_bdv_n}), |
1465 (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*) |
1465 (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*) |
1466 Thm ("nadd_divide_distrib", |
1466 Thm ("add_divide_distrib", |
1467 num_str @{thm add_divide_distrib}) |
1467 num_str @{thm add_divide_distrib}) |
1468 (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z" |
1468 (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z" |
1469 WN051031 DOES NOT BELONG TO HERE*) |
1469 WN051031 DOES NOT BELONG TO HERE*) |
1470 ]; |
1470 ]; |
1471 *} |
1471 *} |