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

_

---

P (theorems)

PAIR_BETA_THM
POLY_0
POLY_ADD
POLY_ADD_CLAUSES
POLY_ADD_RZERO
POLY_BOUND_EXISTS
POLY_CMUL
POLY_CMUL_CLAUSES
POLY_CMUL_MAP
POLY_CONS_EQ
POLY_CONT
POLY_DECOMPOSE
POLY_DECOMPOSE_LEMMA
POLY_DIVIDES_ADD
POLY_DIVIDES_EXP
POLY_DIVIDES_REFL
POLY_DIVIDES_SUB
POLY_DIVIDES_SUB2
POLY_DIVIDES_TRANS
POLY_DIVIDES_ZERO
POLY_ENTIRE
POLY_ENTIRE_LEMMA
POLY_EXP
POLY_EXP_ADD
POLY_EXP_DIVIDES
POLY_EXP_EQ_0
POLY_EXP_PRIME_EQ_0
POLY_INFINITY
POLY_LENGTH_MUL
POLY_LINEAR_DIVIDES
POLY_LINEAR_REM
POLY_MINIMUM_MODULUS
POLY_MINIMUM_MODULUS_DISC
POLY_MUL
POLY_MUL_ASSOC
POLY_MUL_CLAUSES
POLY_MUL_LCANCEL
POLY_NEG
POLY_NEG_CLAUSES
POLY_NORMALIZE
POLY_NORMALIZE_EQ
POLY_NORMALIZE_EQ_LEMMA
POLY_NORMALIZE_ZERO
POLY_OFFSET
POLY_OFFSET_LEMMA
POLY_ORDER
POLY_ORDER_EXISTS
POLY_PRIMES
POLY_PRIME_EQ_0
POLY_REPLICATE_APPEND
POLY_ROOTS_FINITE
POLY_ROOTS_FINITE_LEMMA
POLY_ROOTS_FINITE_SET
POLY_ROOTS_INDEX_LEMMA
POLY_ROOTS_INDEX_LENGTH
POLY_ZERO
POLY_ZERO_LEMMA
parallel
perpendicular
poly
poly_add
poly_cmul
poly_exp
poly_mul
poly_neg
pth
pth_0
pth_1
pth_2
pth_2b
pth_3
pth_4