Crosslinked online reference manual for HOL Light (20th Oct 2023)

• ++
• |||
• >>
• |=>
• --
• |->
• 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
• 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_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_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_num
• print_qterm
• print_qtype
• print_term
• print_thm
• print_to_string
• print_type
• 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
• 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
• 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
• 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