++
|||
>>
|=>
--
|->
a
ABBREV_TAC
ABS
ABS_CONV
ABS_TAC
AC
ACCEPT_TAC
aconv
ADD_ASSUM
allpairs
ALL_CONV
ALL_TAC
ALL_THEN
alpha
alphaorder
ALPHA_CONV
ALPHA
ANTE_RES_THEN
ANTS_TAC
apply
applyd
apply_prover
AP_TERM
AP_TERM_TAC
AP_THM
AP_THM_TAC
ARITH_RULE
ARITH_TAC
ASM
ASM_ARITH_TAC
ASM_CASES_TAC
ASM_FOL_TAC
ASM_INT_ARITH_TAC
ASM_MESON_TAC
ASM_METIS_TAC
ASM_REAL_ARITH_TAC
ASM_REWRITE_RULE
ASM_REWRITE_TAC
ASM_SIMP_TAC
assoc
assocd
ASSOC_CONV
ASSUME
ASSUME_TAC
ASSUM_LIST
atleast
atoms
aty
augment
AUGMENT_SIMPSET
axioms
b
basic_congs
basic_convs
basic_net
basic_prover
basic_rectype_net
basic_rewrites
basic_ss
BETA
BETAS_CONV
BETA_CONV
BETA_RULE
BETA_TAC
binders
BINDER_CONV
BINOP2_CONV
binops
BINOP_CONV
BINOP_TAC
BITS_ELIM_CONV
bndvar
body
BOOL_CASES_TAC
bool_ty
bty
butlast
by
C
CACHE_CONV
can
cases
CASE_REWRITE_TAC
CCONTR
CHANGED_CONV
CHANGED_TAC
CHAR_EQ_CONV
CHEAT_TAC
check
checkpoint
choose
CHOOSE_TAC
CHOOSE_THEN
CHOOSE
chop_list
CLAIM_TAC
CNF_CONV
COMB2_CONV
combine
COMB_CONV
comment_token
compose_insts
concl
CONDS_CELIM_CONV
CONDS_ELIM_CONV
COND_CASES_TAC
COND_ELIM_CONV
CONJ
CONJUNCT1
CONJUNCT2
conjuncts
CONJUNCTS_THEN
CONJUNCTS_THEN2
CONJUNCTS
CONJ_ACI_RULE
CONJ_CANON_CONV
CONJ_PAIR
CONJ_TAC
constants
CONTR
CONTRAPOS_CONV
CONTR_TAC
CONV_RULE
CONV_TAC
metisverb
current_goalstack
curry
decreasing
DEDUCT_ANTISYM_RULE
deep_alpha
define
defined
define_quotient_type
define_type
define_type_raw
definitions
delete_parser
delete_user_printer
denominator
DENUMERAL
DEPTH_BINOP_CONV
DEPTH_CONV
DEPTH_SQCONV
derive_nonschematic_inductive_relations
derive_strong_induction
DESTRUCT_TAC
dest_abs
dest_binary
dest_binder
dest_binop
dest_char
dest_comb
dest_cond
dest_conj
dest_cons
dest_const
dest_disj
dest_eq
dest_exists
dest_finty
dest_forall
dest_fun_ty
dest_gabs
dest_iff
dest_imp
dest_intconst
dest_let
dest_list
dest_neg
dest_numeral
dest_pair
dest_realintconst
dest_select
dest_setenum
dest_small_numeral
dest_string
dest_thm
dest_type
dest_uexists
dest_var
dest_vartype
DIMINDEX_CONV
DIMINDEX_TAC
DISCH
DISCH_ALL
DISCH_TAC
DISCH_THEN
DISJ1
DISJ1_TAC
DISJ2
DISJ2_TAC
disjuncts
DISJ_ACI_RULE
DISJ_CANON_CONV
DISJ_CASES
DISJ_CASES_TAC
DISJ_CASES_THEN
DISJ_CASES_THEN2
distinctness
distinctness_store
DNF_CONV
dom
do_list
dpty
e
el
elistof
empty_net
empty_ss
end_itlist
enter
EQF_ELIM
EQF_INTRO
EQT_ELIM
EQT_INTRO
equals_goal
equals_thm
EQ_IMP_RULE
EQ_MP
EQ_TAC
ETA_CONV
EVERY
EVERY_ASSUM
EVERY_CONV
EVERY_TCL
exactly
EXISTENCE
exists
EXISTS_EQUATION
EXISTS_TAC
EXISTS
EXPAND_CASES_CONV
EXPAND_NSUM_CONV
EXPAND_SUM_CONV
EXPAND_TAC
explode
extend_basic_congs
extend_basic_convs
extend_basic_rewrites
extend_rectype_net
fail
FAIL_TAC
file_of_string
file_on_path
filter
find
FIND_ASSUM
find_index
find_path
find_term
find_terms
finished
FIRST
FIRST_ASSUM
FIRST_CONV
FIRST_TCL
FIRST_X_ASSUM
fix
FIX_TAC
flat
flush_goalstack
foldl
foldr
follow_path
forall
forall2
FORALL_UNWIND_CONV
frees
freesin
freesl
FREEZE_THEN
free_in
funpow
F_F
f_f_
g
GABS_CONV
gcd
gcd_num
GEN
GENERAL_REWRITE_CONV
GENL
genvar
GEN_ALL
GEN_ALPHA_CONV
GEN_BETA_CONV
GEN_MESON_TAC
GEN_NNF_CONV
GEN_PART_MATCH
GEN_REAL_ARITH
GEN_REWRITE_CONV
GEN_REWRITE_RULE
GEN_REWRITE_TAC
GEN_SIMPLIFY_CONV
GEN_TAC
get_const_type
get_infix_status
get_type_arity
graph
GSYM
HAS_SIZE_CONV
HAS_SIZE_DIMINDEX_RULE
hd
help
help_path
hide_constant
HIGHER_REWRITE_CONV
HINT_EXISTS_TAC
hol_dir
hol_expand_directory
hol_version
hyp
HYP_TAC
HYP
I
ideal_cofactors
ignore_constant_varstruct
implode
IMP_ANTISYM_RULE
IMP_RES_THEN
IMP_REWRITE_TAC
IMP_REWR_CONV
IMP_TRANS
increasing
index
inductive_type_store
INDUCT_TAC
infixes
injectivity
injectivity_store
insert
insert'
inst
installed_parsers
install_parser
install_user_printer
instantiate
INSTANTIATE_ALL
instantiate_casewise_recursion
INSTANTIATE
inst_goal
INST_TYPE
INST
INTEGER_RULE
INTEGER_TAC
intersect
INTRO_TAC
INT_ABS_CONV
INT_ADD_CONV
INT_ARITH
INT_ARITH_TAC
INT_EQ_CONV
INT_GE_CONV
INT_GT_CONV
int_ideal_cofactors
INT_LE_CONV
INT_LT_CONV
INT_MAX_CONV
INT_MIN_CONV
INT_MUL_CONV
INT_NEG_CONV
INT_OF_REAL_THM
INT_POLY_CONV
INT_POW_CONV
INT_REDUCE_CONV
INT_RED_CONV
INT_REM_DOWN_CONV
INT_RING
INT_SGN_CONV
INT_SUB_CONV
isalnum
isalpha
isbra
isnum
ISPEC
ISPECL
issep
isspace
issymb
is_abs
is_binary
is_binder
is_binop
is_comb
is_cond
is_conj
is_cons
is_const
is_disj
is_eq
is_exists
is_forall
is_gabs
is_hidden
is_iff
is_imp
is_intconst
is_let
is_list
is_neg
is_numeral
is_pair
is_prefix
is_ratconst
is_realintconst
is_reserved_word
is_select
is_setenum
is_type
is_uexists
is_undefined
is_var
is_vartype
it
ITAUT
ITAUT_TAC
itlist
itlist2
K
LABEL_TAC
LAMBDA_ELIM_CONV
LAND_CONV
last
lcm_num
LEANCOP
LEANCOP_TAC
leftbin
length
let_CONV
LET_TAC
lex
LE_IMP
lhand
lhs
lift_function
lift_theorem
listof
LIST_CONV
LIST_INDUCT_TAC
list_mk_abs
list_mk_binop
list_mk_comb
list_mk_conj
list_mk_disj
list_mk_exists
list_mk_forall
list_mk_gabs
list_mk_icomb
loaded_files
loads
loadt
load_on_path
load_path
lookup
make_args
make_overloadable
many
map
map2
mapf
mapfilter
MAP_EVERY
MAP_FIRST
MATCH_ACCEPT_TAC
MATCH_CONV
MATCH_MP
MATCH_MP_TAC
mem
mem'
merge
mergesort
merge_nets
MESON
meson_brand
meson_chatty
meson_dcutin
meson_depth
meson_prefine
meson_skew
meson_split_limit
MESON_TAC
META_EXISTS_TAC
META_SPEC_TAC
METIS
metisverb
METIS_TAC
mk_abs
mk_binary
mk_binder
mk_binop
MK_BINOP
mk_char
mk_comb
MK_COMB_TAC
MK_COMB
mk_cond
mk_conj
MK_CONJ
mk_cons
mk_const
mk_disj
MK_DISJ
mk_eq
mk_exists
MK_EXISTS
mk_finty
mk_flist
mk_forall
MK_FORALL
mk_fset
mk_fthm
mk_fun_ty
mk_gabs
mk_goalstate
mk_icomb
mk_iff
mk_imp
mk_intconst
mk_let
mk_list
mk_mconst
mk_neg
mk_numeral
mk_pair
mk_primed_var
mk_prover
mk_realintconst
mk_rewrites
mk_select
mk_setenum
mk_small_numeral
mk_string
mk_thm
mk_type
mk_uexists
mk_var
mk_vartype
MOD_DOWN_CONV
monotonicity_theorems
MONO_TAC
MP
MP_CONV
MP_TAC
name
NAME_ASSUMS_TAC
name_of
NANOCOP
NANOCOP_TAC
needs
net_of_cong
net_of_conv
net_of_thm
new_axiom
new_basic_definition
new_basic_type_definition
new_constant
new_definition
new_inductive_definition
new_inductive_set
new_recursive_definition
new_specification
new_type
new_type_abbrev
new_type_definition
NNFC_CONV
NNF_CONV
nothing
NOT_ELIM
NOT_INTRO
NO_CONV
NO_TAC
NO_THEN
nsplit
null_inst
null_meta
NUMBER_RULE
NUMBER_TAC
numdom
numerator
NUMSEG_CONV
num_0
num_1
num_10
num_2
NUM_ADD_CONV
NUM_CANCEL_CONV
num_CONV
NUM_DIV_CONV
NUM_EQ_CONV
NUM_EVEN_CONV
NUM_EXP_CONV
NUM_FACT_CONV
NUM_GE_CONV
NUM_GT_CONV
NUM_LE_CONV
NUM_LT_CONV
NUM_MAX_CONV
NUM_MIN_CONV
NUM_MOD_CONV
NUM_MULT_CONV
NUM_NORMALIZE_CONV
NUM_ODD_CONV
num_of_string
NUM_PRE_CONV
NUM_REDUCE_CONV
NUM_REDUCE_TAC
NUM_RED_CONV
NUM_REL_CONV
NUM_RING
NUM_SIMPLIFY_CONV
NUM_SUB_CONV
NUM_SUC_CONV
NUM_TO_INT_CONV
o
occurs_in
omit
ONCE_ASM_REWRITE_RULE
ONCE_ASM_REWRITE_TAC
ONCE_ASM_SIMP_TAC
ONCE_DEPTH_CONV
ONCE_DEPTH_SQCONV
ONCE_REWRITE_CONV
ONCE_REWRITE_RULE
ONCE_REWRITE_TAC
ONCE_SIMPLIFY_CONV
ONCE_SIMP_CONV
ONCE_SIMP_RULE
ONCE_SIMP_TAC
ORDERED_IMP_REWR_CONV
ORDERED_REWR_CONV
ORELSE
ORELSEC
orelsec_
orelse_
ORELSE_TCL
orelse_tcl_
overload_interface
override_interface
p
parses_as_binder
parse_as_binder
parse_as_infix
parse_as_prefix
parse_inductive_type_specification
parse_preterm
parse_pretype
parse_term
parse_type
partition
PART_MATCH
PATH_CONV
PAT_CONV
PINST
POP_ASSUM
POP_ASSUM_LIST
possibly
pow10
pow2
pp_print_fpf
pp_print_num
pp_print_qterm
pp_print_qtype
pp_print_term
pp_print_thm
pp_print_type
prebroken_binops
prefixes
PRENEX_CONV
PRESIMP_CONV
preterm_of_term
pretype_of_type
print_all_thm
print_fpf
print_goal
print_goalstack
print_goal_hyp_max_boxes
PRINT_GOAL_TAC
print_num
print_qterm
print_qtype
print_term
PRINT_TERM_CONV
print_thm
print_to_string
print_type
print_types_of_subterms
print_unambiguous_comprehensions
prioritize_int
prioritize_num
prioritize_overload
prioritize_real
PROP_ATOM_CONV
prove
prove_cases_thm
prove_constructors_distinct
prove_constructors_injective
prove_general_recursive_function_exists
PROVE_HYP
prove_inductive_relations_exist
prove_monotonicity_hyps
prove_recursive_functions_exist
PURE_ASM_REWRITE_RULE
PURE_ASM_REWRITE_TAC
PURE_ASM_SIMP_TAC
PURE_ONCE_ASM_REWRITE_RULE
PURE_ONCE_ASM_REWRITE_TAC
PURE_ONCE_REWRITE_CONV
PURE_ONCE_REWRITE_RULE
PURE_ONCE_REWRITE_TAC
pure_prove_recursive_function_exists
PURE_REWRITE_CONV
PURE_REWRITE_RULE
PURE_REWRITE_TAC
PURE_SIMP_CONV
PURE_SIMP_RULE
PURE_SIMP_TAC
qmap
quotexpander
r
ran
rand
RAND_CONV
rator
RATOR_CONV
rat_of_term
REAL_ARITH
REAL_ARITH_TAC
REAL_FIELD
real_ideal_cofactors
REAL_IDEAL_CONV
REAL_INT_ABS_CONV
REAL_INT_ADD_CONV
REAL_INT_EQ_CONV
REAL_INT_GE_CONV
REAL_INT_GT_CONV
REAL_INT_LE_CONV
REAL_INT_LT_CONV
REAL_INT_MUL_CONV
REAL_INT_NEG_CONV
REAL_INT_POW_CONV
REAL_INT_RAT_CONV
REAL_INT_REDUCE_CONV
REAL_INT_RED_CONV
REAL_INT_SUB_CONV
REAL_LET_IMP
REAL_LE_IMP
REAL_LINEAR_PROVER
REAL_POLY_ADD_CONV
REAL_POLY_CONV
REAL_POLY_MUL_CONV
REAL_POLY_NEG_CONV
REAL_POLY_POW_CONV
REAL_POLY_SUB_CONV
REAL_RAT_ABS_CONV
REAL_RAT_ADD_CONV
REAL_RAT_DIV_CONV
REAL_RAT_EQ_CONV
REAL_RAT_GE_CONV
REAL_RAT_GT_CONV
REAL_RAT_INV_CONV
REAL_RAT_LE_CONV
REAL_RAT_LT_CONV
REAL_RAT_MAX_CONV
REAL_RAT_MIN_CONV
REAL_RAT_MUL_CONV
REAL_RAT_NEG_CONV
REAL_RAT_POW_CONV
REAL_RAT_REDUCE_CONV
REAL_RAT_RED_CONV
REAL_RAT_SGN_CONV
REAL_RAT_SUB_CONV
REAL_RING
RECALL_ACCEPT_TAC
REDEPTH_CONV
REDEPTH_SQCONV
reduce_interface
refine
REFL
REFL_TAC
REFUTE_THEN
remark
REMARK_TAC
remove
remove_interface
REMOVE_THEN
remove_type_abbrev
repeat
REPEATC
REPEAT_GTCL
REPEAT_TCL
REPEAT
replicate
REPLICATE_TAC
report
report_timing
reserved_words
reserve_words
retypecheck
rev
reverse_interface_mapping
rev_assoc
rev_assocd
rev_itlist
rev_itlist2
rev_splitlist
REWRITES_CONV
REWRITE_CONV
REWRITE_RULE
REWRITE_TAC
REWR_CONV
rhs
rightbin
RIGHT_BETAS
RING
RING_AND_IDEAL_CONV
rotate
RULE_ASSUM_TAC
search
SELECT_CONV
SELECT_ELIM_TAC
SELECT_RULE
self_destruct
SEMIRING_NORMALIZERS_CONV
SEQ_IMP_REWRITE_TAC
setify
set_basic_congs
set_basic_convs
set_basic_rewrites
set_eq
set_goal
SET_RULE
SET_TAC
set_verbose_symbols
shareout
SIMPLE_CHOOSE
SIMPLE_DISJ_CASES
SIMPLE_EXISTS
SIMPLIFY_CONV
SIMP_CONV
SIMP_RULE
SIMP_TAC
SKOLEM_CONV
some
sort
SPEC
SPECL
SPEC_ALL
SPEC_TAC
SPEC_VAR
splitlist
ss_of_congs
ss_of_conv
ss_of_maker
ss_of_prover
ss_of_provers
ss_of_thms
startup_banner
strings_of_file
STRING_EQ_CONV
string_of_file
string_of_term
string_of_thm
string_of_type
striplist
strip_abs
STRIP_ASSUME_TAC
strip_comb
strip_exists
strip_forall
strip_gabs
STRIP_GOAL_THEN
strip_ncomb
STRIP_TAC
STRIP_THM_THEN
STRUCT_CASES_TAC
STRUCT_CASES_THEN
SUBGOAL_TAC
SUBGOAL_THEN
SUBLET_CONV
SUBS
subset
subst
SUBST1_TAC
SUBST_ALL_TAC
SUBST_VAR_TAC
SUBS_CONV
subtract
subtract'
SUB_CONV
SYM
SYM_CONV
TAC_PROOF
TARGET_REWRITE_TAC
TAUT
temp_path
term_match
term_of_preterm
term_of_rat
term_order
term_type_unify
term_unify
term_union
THEN
THENC
thenc_
THENL
thenl_
then_
THEN_TCL
then_tcl_
theorems
the_definitions
the_implicit_types
the_inductive_definitions
the_inductive_types
the_interface
the_overload_skeletons
the_specifications
the_type_definitions
thm_frees
time
tl
TOP_DEPTH_CONV
TOP_DEPTH_SQCONV
top_goal
top_realgoal
TOP_SWEEP_CONV
TOP_SWEEP_SQCONV
top_thm
TRANS
TRANS_TAC
TRY
tryapplyd
tryfind
TRY_CONV
try_user_parser
try_user_printer
types
type_abbrevs
type_invention_error
type_invention_warning
type_match
type_of
type_of_pretype
type_subst
type_unify
type_vars_in_term
typify_universal_set
tysubst
tyvars
uncurry
undefine
undefined
UNDISCH
UNDISCH_ALL
UNDISCH_TAC
UNDISCH_THEN
unhide_constant
UNIFY_ACCEPT_TAC
union
unions
unions'
union'
uniq
unparse_as_binder
unparse_as_infix
unparse_as_prefix
unreserve_words
unset_jrh_lexer
unset_then_multiple_subgoals
unset_verbose_symbols
unspaced_binops
UNWIND_CONV
unzip
use_file
use_file_raise_failure
USE_THEN
VALID
variables
variant
variants
verbose
vfree_in
vsubst
W
warn
WEAK_CNF_CONV
WEAK_DNF_CONV
WF_INDUCT_TAC
X_CHOOSE_TAC
X_CHOOSE_THEN
X_GEN_TAC
X_META_EXISTS_TAC
zip