HOL html
| Files Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ |
| Theorems Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ |
D (theorems)
DIFF_DIFF2DIFF_INTER
DIFF_SUBSET
DIFF_SURJ
DIVIDE
DIVIDE_DIVIDE
DIVIDE_EQ
DIVIDE_PROD
DIVIDE_PROD2
DIVIDE_SUM
DIVIDE_SUMMAND
DOMAIN_EMPTY
DOMAIN_INSERT
D_EUCLID_BOUND
d_euclid_bound2
d_euclid_cis
d_euclid_cis_ineq
d_euclid_eq_arg
d_euclid_floor
d_euclid_mk_segment
d_euclid_n
d_euclid_point
d_euclid_pointI_pos
d_euclid_pos
d_euclid_pos2
d_euclid_pow2
d_euclid_zero
d_euclidpq
degree4_vertex_hv
degree_vertex_annulus
degree_vertex_disk
degree_vertex_disk_ver2
delete_empty
delete_inters
delta_partition_lemma
delta_partition_lemma_ver2
delta_pos_arch
dense_open
dense_subset
deriv
deriv2
dest_pt_point
diff_pow1
diff_unchange
dirac_0
dirac_delta
disk_endpoint
disk_endpoint_gen
disk_endpoint_outer
dot_comm
dot_euclid
dot_linear
dot_linear2
dot_linear2_euclidean
dot_linear_euclidean
dot_lzero
dot_minus_linear
dot_minus_linear2
dot_minus_linear2_euclidean
dot_minus_linear_euclidean
dot_neg
dot_neg2
dot_nonneg
dot_point
dot_rzero
dot_scale
dot_scale2
dot_scale2_euclidean
dot_scale_euclidean
dot_updim
dot_zero
dot_zero_euclidean
drop0
drop1
drop2
drop3
drop_ant_tac_example