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 | _ |
O (theorems)
OR_EXISTS_THModd_bounded
odd_bounded_subset
old_prove
old_prove_by_refinement
one_over_plus1
open_EMPTY
open_and_closed
open_ball_center
open_ball_dist
open_ball_empty
open_ball_inter
open_ball_intersect
open_ball_nbd
open_ball_neg_radius
open_ball_nest
open_ball_nonempty
open_ball_nonempty_center
open_ball_open
open_ball_path
open_ball_star
open_ball_sub_closed
open_ball_subset
open_ball_subspace
open_closed
open_half_plane2D_FLT
open_half_plane2D_FLT_convex
open_half_plane2D_FLT_open
open_half_plane2D_LTF
open_half_plane2D_LTF_convex
open_half_plane2D_LTF_open
open_half_plane2D_LTS
open_half_plane2D_LTS_convex
open_half_plane2D_LTS_open
open_half_plane2D_SLT
open_half_plane2D_SLT_convex
open_half_plane2D_SLT_open
open_half_space_convex
open_half_space_diff
open_half_space_euclid
open_half_space_open
open_half_space_scale
open_induced
open_inters
open_nbd
open_real_interval
openball_convex
openball_mk_segment_end
order_imp_psegment
order_imp_psegment_shift
order_lt_imp_psegment
other_end_prop
outer_segment_even