HOL IDENTIFIER 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

Symbolic Identifiers

## (value; Lib)
&& (value; bossLib, simpLib)
* (value; Arbint, Arbnum)
+ (value; Arbint, Arbnum)
++ (value; bossLib, simpLib)
- (value; Arbint, Arbnum)
-- (value; Parse)
--> (value; Type)
< (value; Arbint, Arbnum)
<= (value; Arbint, Arbnum)
== (value; Parse)
> (value; Arbint, Arbnum)
>= (value; Arbint, Arbnum)
?> (value; Lib)
|-> (value; Lib)
|> (value; liteLib)
~ (value; Arbint)

A

A (value; Lib)
Abbr (value; BasicProvers)
ABBREV (constructor; DefnBase)
Abbrev (structure)
ABBREV_TAC (value; Q)
ABBRS_THEN (value; Q)
Abs (constructor; Count, Preterm)
ABS (value; Q, Thm)
abs (value; Arbint)
ABS_CONV (value; Conv, liteLib)
absval_tm (value; intSyntax)
Absyn (structure)
absyn (type; Absyn, Defn)
Absyn (value; Parse)
absyn_to_preterm (value; Parse)
absyn_to_term (value; Parse)
AC (structure)
AC (value; AC, bossLib, simpLib)
AC_CANON_CONV (value; AC)
AC_CANON_GEN_CONV (value; AC)
AC_CONV (value; Conv, Q)
ac_ss (value; simpLib)
ACCEPT_TAC (value; Tactic, jrhTactics)
accessors_of (value; TypeBase, TypeBasePure)
aconv (value; Term)
add (value; TypeBasePure, goalstackLib)
add_assoc (value; liteLib)
ADD_ASSUM (value; Drule)
add_bare_numeral_form (value; Parse)
add_binder (value; Parse)
add_const (value; Parse)
ADD_CONV (value; reduceLib)
add_conv (value; computeLib)
add_convs (value; computeLib)
add_funs (value; computeLib)
add_implicit_rewrites (value; Ho_Rewrite, Rewrite)
add_infix (value; Parse)
add_infix_type (value; Parse)
add_listform (value; Parse)
add_mono_thm (value; IndDefLib)
add_numeral_form (value; Parse)
add_persistent_funs (value; computeLib)
add_record_field (value; Parse)
add_record_fupdate (value; Parse)
add_rewrites (value; Rewrite)
add_rule (value; Parse)
add_tag (value; Thm)
add_thms (value; computeLib)
add_type (value; Parse)
add_user_printer (value; Parse)
ADDL_CANON_CONV (value; numSimps)
ADDR_CANON_CONV (value; numSimps)
adjoin_to_theory (value; Theory)
after_new_theory (value; Theory)
all (value; Lib)
all2 (value; Lib)
all_consts (value; Term)
ALL_CONV (value; Conv)
all_distinct_tm (value; listSyntax)
ALL_TAC (value; Tactical, jrhTactics)
ALL_THEN (value; Thm_cont)
all_vars (value; Term)
all_varsl (value; Term)
allow_schema_definition (value; Globals)
allowed_term_constant (value; Lexis)
allowed_type_constant (value; Lexis)
allowed_user_type_var (value; Lexis)
Alpha (constructor; Count)
ALPHA (value; Thm)
alpha (value; Type, liteLib)
ALPHA_CONV (value; Drule)
alphabet (value; Lexis)
alphanumerics (value; Lexis)
alt_zero_tm (value; numSyntax)
Always (value; Parse)
ancestry (value; Theory, hol88Lib)
AND_CONV (value; reduceLib)
AND_EXISTS_CONV (value; Conv)
AND_FORALL_CONV (value; Conv)
AND_PEXISTS_CONV (value; PairRules)
AND_PFORALL_CONV (value; PairRules)
ANTE_CONJ_CONV (value; Conv)
ANTE_RES_THEN (value; Thm_cont)
Antiq (constructor; Preterm)
AP_TERM (value; Q, Thm)
AP_TERM_TAC (value; Tactic)
AP_THM (value; Q, Thm)
AP_THM_TAC (value; Tactic)
apiDefine (value; TotalDefn)
apiDefineq (value; TotalDefn)
apidefn (type; TotalDefn)
APP (constructor; Absyn)
append (value; Lib)
append_tm (value; listLib, listSyntax)
appi (value; Lib)
apply (value; Count)
apropos (value; DB)
ApTerm (constructor; Count)
ApThm (constructor; Count)
AQ (constructor; Absyn)
arb (value; boolSyntax)
Arbint (structure)
Arbnum (structure)
argv (value; Portable)
ARITH_AC_ss (value; numSimps)
arith_cache (value; numSimps, realSimps)
ARITH_CONV (value; intLib, numLib)
ARITH_DP_ss (value; numSimps)
ARITH_PROVE (value; intLib, numLib)
ARITH_RWTS_ss (value; numSimps)
ARITH_ss (value; bossLib, numSimps)
arith_ss (value; bossLib)
ARITH_TAC (value; intLib, numLib)
AroundEachPhrase (value; Parse)
AroundSameName (value; Parse)
AroundSamePrec (value; Parse)
asList (value; Arbnum)
ASM_CASES_TAC (value; Q, Tactic)
ASM_MESON_TAC (value; mesonLib)
ASM_REWRITE_RULE (value; Ho_Rewrite, Rewrite)
ASM_REWRITE_TAC (value; Ho_Rewrite, Rewrite)
ASM_SIMP_RULE (value; simpLib)
ASM_SIMP_TAC (value; bossLib, simpLib)
ASM_TAUT_TAC (value; tautLib)
assert (value; Lib)
assert_exn (value; Lib)
assoc (value; Lib, hol88Lib)
assoc1 (value; Lib)
assoc2 (value; Lib)
ASSOC_CONV (value; AC)
assoc_tm (value; boolSyntax)
associate_restriction (value; Parse)
associativity (type; Parse)
ASSUM_LIST (value; Tactical, jrhTactics)
Assume (constructor; Count)
ASSUME (value; Q, Thm)
ASSUME_TAC (value; Tactic, jrhTactics)
assums (type; PrimitiveBddRules)
AST (type; Datatype)
attempt_theory_extension (value; Theory)
augment_srw_ss (value; BasicProvers, bossLib)
auto_import_definitions (value; computeLib)
aux_defn (value; Defn)
ax_tag (value; Tag)
Axiom (constructor; Count)
axiom (value; DB)
axiom_of (value; TypeBase, TypeBasePure)
axiom_of0 (value; TypeBase, TypeBasePure)
axioms (value; DB)
axioms_of (value; Tag)
Axm (constructor; DB)

B

B (value; Lib)
b (value; goalstackLib)
BACKCHAIN_TAC (value; InductiveDefinition)
backup (value; goalstackLib)
BAG_AC_ss (value; bagLib, bagSimps)
BAG_DIFF_tm (value; bagLib, bagSyntax)
BAG_INSERT_tm (value; bagLib, bagSyntax)
BAG_ss (value; bagLib, bagSimps)
bag_ty (value; bagLib, bagSyntax)
BAG_UNION_tm (value; bagLib, bagSyntax)
bagLib (structure)
bagSimps (structure)
bagSyntax (structure)
base_type (value; bagLib, bagSyntax)
basic_diffs (value; realLib)
BasicProvers (structure)
bdd (type; DerivedBddRules)
BddApConv (value; DerivedBddRules)
BddAppall (value; PrimitiveBddRules)
BddAppallError (exception; PrimitiveBddRules)
BddAppex (value; PrimitiveBddRules)
BddAppexError (exception; PrimitiveBddRules)
BddApReplace (value; DerivedBddRules)
BddApReplaceError (exception; DerivedBddRules)
BddApRestrict (value; DerivedBddRules)
BddApRestrictError (exception; DerivedBddRules)
BddApSubst (value; DerivedBddRules)
BddApSubstError (exception; DerivedBddRules)
BddApThm (value; DerivedBddRules)
BddAssume (value; DerivedBddRules)
BddCompose (value; PrimitiveBddRules)
BddComposeError (exception; PrimitiveBddRules)
BddCon (value; PrimitiveBddRules)
BddDisch (value; PrimitiveBddRules)
BddEqMp (value; PrimitiveBddRules)
BddEqMpError (exception; PrimitiveBddRules)
BddEqualTest (value; DerivedBddRules)
BddExists (value; PrimitiveBddRules)
BddExistsError (exception; PrimitiveBddRules)
BddExtendVarmap (value; PrimitiveBddRules)
BddExtendVarmapError (exception; PrimitiveBddRules)
BddfindModel (value; PrimitiveBddRules)
BddfindModelError (exception; PrimitiveBddRules)
BddForall (value; PrimitiveBddRules)
BddForallError (exception; PrimitiveBddRules)
BddFreevarsContractVarmap (value; PrimitiveBddRules)
BddFreevarsContractVarmapError (exception; PrimitiveBddRules)
BddIte (value; PrimitiveBddRules)
BddIteError (exception; PrimitiveBddRules)
BddListCompose (value; PrimitiveBddRules)
BddListComposeError (exception; PrimitiveBddRules)
BddNot (value; PrimitiveBddRules)
bddop (type; DerivedBddRules)
BddOp (value; PrimitiveBddRules)
BddOpError (exception; PrimitiveBddRules)
BddReplace (value; PrimitiveBddRules)
BddReplaceError (exception; PrimitiveBddRules)
BddRestrict (value; PrimitiveBddRules)
BddRestrictError (exception; PrimitiveBddRules)
BddRhsOracle (value; DerivedBddRules)
BddSatone (value; DerivedBddRules)
BddSatoneError (exception; DerivedBddRules)
BddSimplify (value; PrimitiveBddRules)
BddSimplifyError (exception; PrimitiveBddRules)
BddSubst (value; DerivedBddRules)
BddSupportContractVarmap (value; PrimitiveBddRules)
BddSupportContractVarmapError (exception; PrimitiveBddRules)
BddThmOracle (value; PrimitiveBddRules)
BddThmOracleError (exception; PrimitiveBddRules)
bddToTerm (value; DerivedBddRules)
bddToTermError (exception; DerivedBddRules)
BddVar (value; PrimitiveBddRules)
BddVarError (exception; PrimitiveBddRules)
BeginFinalBlock (value; Parse)
BEQ_CONV (value; reduceLib)
Beta (constructor; Count)
Beta (value; Thm)
beta (value; Type)
BETA_CONV (value; Q, Thm)
beta_conv (value; Term)
BETA_RULE (value; Conv)
BETA_TAC (value; Tactic)
BETA_VAR (value; Drule)
big_record_size (value; Datatype)
biginter_tm (value; pred_setSyntax)
bigunion_tm (value; pred_setSyntax)
bij_tm (value; pred_setSyntax)
Binder (constructor; Parse)
BINDER_CONV (value; Conv, liteLib)
bindl (value; DB)
BINOP_CONV (value; Conv, liteLib)
BINOP_TAC (value; Tactic)
binops (value; liteLib)
bit1_tm (value; numSyntax)
bit2_tm (value; numSyntax)
BIT_CONV (value; wordLib)
block_info (type; Parse)
body (value; Term)
BODY_CONJUNCTS (value; Drule)
BODY_CONV (value; Canon, liteLib)
bool (value; Type)
bool_case (value; boolSyntax)
BOOL_CASES_TAC (value; Tactic)
bool_compset (value; computeLib)
bool_EQ_CONV (value; Conv)
bool_monoset (value; InductiveDefinition)
bool_rewrites (value; Rewrite)
BOOL_ss (value; boolSimps)
bool_ss (value; BasicProvers, boolSimps, bossLib)
boolSimps (structure)
boolSyntax (structure)
bossLib (structure)
BOUNDED_EXISTS_CONV (value; numLib)
BOUNDED_FORALL_CONV (value; numLib)
bounded_tm (value; boolSyntax)
break_style (type; Portable)
BreakSpace (value; Parse)
BUILD (constructor; TotalDefn)
build_log_dir (value; Systeml)
build_log_file (value; Systeml)
build_tyinfos (value; Datatype)
butlast (value; Lib)
bvar (value; Term)
by (value; SingleStep, bossLib, jrhTactics)
bys (value; jrhTactics)

C

C (value; Lib)
C_tm (value; combinSyntax)
cache (type; bagLib, bagSimps)
cache (value; mesonLib)
CACHED_ARITH (value; numSimps)
can (value; Lib)
CANCEL_CONV (value; bagLib, bagSimps)
Canon (structure)
Canon_Port (structure)
card_tm (value; pred_setSyntax)
case_cong_of (value; TypeBase, TypeBasePure)
case_cong_thm (value; Prim_rec)
case_const_of (value; TypeBase, TypeBasePure)
case_def_of (value; TypeBase, TypeBasePure)
CASE_SIMP_CONV (value; SingleStep)
CASE_TAC (value; SingleStep, bossLib)
Cases (value; SingleStep, bossLib)
Cases_on (value; SingleStep, bossLib)
Cases_on_word (value; wordsLib)
CASES_THENL (value; Thm_cont)
Cases_word (value; wordsLib)
CB (value; hol88Lib)
CBV_CONV (value; computeLib)
Ccontr (constructor; Count)
CCONTR (value; Thm)
CCONTR_TAC (value; Tactic)
cd (value; Portable)
CHANGED_CONV (value; Conv)
CHANGED_TAC (value; Tactical)
char_EQ_CONV (value; stringLib)
char_rewrites (value; stringSimps)
char_ty (value; stringLib, stringSyntax)
chatting (value; goalstackLib, mesonLib)
CHECK_ASSUME_TAC (value; Tactic)
checking_const_names (value; Globals)
checking_type_names (value; Globals)
choice_tm (value; pred_setSyntax)
Choose (constructor; Count)
CHOOSE (value; Thm)
CHOOSE_TAC (value; Tactic, jrhTactics)
CHOOSE_THEN (value; Thm_cont)
chop_list (value; liteLib)
chr_tm (value; stringLib, stringSyntax)
cinst (value; TypeBasePure)
class (type; DB)
CLEANUP_DEF_CNF_CONV (value; defCNF)
clear_arith_caches (value; numSimps)
clear_overloads_on (value; Parse)
clear_prefs_for_term (value; Parse)
close_in (value; Portable)
close_out (value; Portable)
Closefix (value; Parse)
cmp (type; Lib)
CNF_CONV (value; Canon)
CNF_REFUTE (value; Canon)
CNF_THEN_REFUTE (value; Canon)
Co (value; hol88Lib)
COMB (constructor; Psyntax, Rsyntax)
Comb (constructor; Preterm)
COMB2_CONV (value; liteLib)
COMB2_QCONV (value; liteLib)
COMB_CONV (value; Conv, liteLib)
COMB_QCONV (value; liteLib)
combine (value; Lib)
combinSyntax (structure)
comm_tm (value; boolSyntax)
comma_tm (value; pairLib, pairSyntax)
commafy (value; Lib)
compare (value; Arbint, Term, Type)
compl_tm (value; pred_setSyntax)
completeInduct_on (value; SingleStep, bossLib)
compset (type; computeLib)
computeFixedpoint (value; DerivedBddRules)
computeFixedpointError (exception; DerivedBddRules)
computeLib (structure)
computeTrace (value; DerivedBddRules)
computeTraceError (exception; DerivedBddRules)
concat (value; Lib)
concl (value; Thm)
COND_CASES_TAC (value; Tactic)
COND_CONV (value; Conv, reduceLib)
COND_elim_ss (value; boolSimps)
conditional (value; boolSyntax)
Cong (value; bossLib, simpLib)
CONG_ss (value; boolSimps)
Conj (constructor; Count)
CONJ (value; Thm)
CONJ_ACI (value; AC)
CONJ_DISCH (value; Drule)
CONJ_DISCHL (value; Drule)
CONJ_FORALL_CONV (value; unwindLib)
CONJ_FORALL_ONCE_CONV (value; unwindLib)
CONJ_FORALL_RIGHT_RULE (value; unwindLib)
CONJ_LIST (value; Drule)
CONJ_PAIR (value; Drule)
CONJ_SET_CONV (value; Drule)
CONJ_ss (value; boolSimps)
CONJ_TAC (value; Tactic)
Conjunct1 (constructor; Count)
CONJUNCT1 (value; Thm)
Conjunct2 (constructor; Count)
CONJUNCT2 (value; Thm)
conjunction (value; boolSyntax)
CONJUNCTS (value; Drule)
conjuncts (value; hol88Lib)
CONJUNCTS_CONV (value; Drule)
CONJUNCTS_THEN (value; Thm_cont, jrhTactics)
CONJUNCTS_THEN2 (value; Thm_cont)
cons (value; Lib)
cons_tm (value; listLib, listSyntax)
CONST (constructor; Psyntax, Rsyntax)
Const (constructor; Preterm)
const_eq_ref (value; Defn)
constants (value; Theory)
Constrained (constructor; Preterm)
constructor (type; Datatype, ind_types)
constructors_of (value; TypeBase, TypeBasePure)
CONTR (value; Drule)
CONTR_TAC (value; Tactic, jrhTactics)
CONTRAPOS (value; Drule)
CONTRAPOS_CONV (value; Conv)
Conv (structure)
conv (type; Abbrev, Canon, ratLib, realLib, temporalLib, unwindLib)
CONV_OF_PROVER (value; Canon)
CONV_RULE (value; Conv)
CONV_TAC (value; Tactic)
CONV_THEN_REFUTE (value; Canon)
convdata (type; simpLib)
convert (value; jrhTactics)
Cooper (structure)
COOPER_CONV (value; Cooper, intLib)
COOPER_PROVE (value; Cooper, intLib)
COOPER_TAC (value; Cooper, intLib)
COPY (constructor; TypeBasePure)
Count (structure)
count_tm (value; pred_setSyntax)
counting_thms (value; Count)
cross_tm (value; pred_setSyntax)
ctxt (type; numSimps)
CTXT_ARITH (value; numSimps)
current_axioms (value; Theory)
current_definitions (value; Theory)
current_grammars (value; Parse)
current_lgrms (value; Parse)
current_theorems (value; Theory)
current_theory (value; Theory)
current_trace (value; Feedback)
curry (value; Lib)
CURRY_CONV (value; PairRules)
CURRY_EXISTS_CONV (value; PairRules)
CURRY_FORALL_CONV (value; PairRules)
curry_tm (value; pairLib, pairSyntax)

D

data (type; DB)
Datatype (structure)
DB (structure)
dcnfgv (value; defCNF)
dcutin (value; mesonLib)
dec (value; Portable)
DECIDE (value; bossLib)
decide_pure_presburger_term (value; Cooper)
DECIDE_TAC (value; bossLib)
declare_ring (value; ringLib)
decls (value; Term, Type)
Def (constructor; DB)
DEF_CNF_CONV (value; defCNF)
DEF_CNF_VECTOR_CONV (value; defCNF)
DEF_NNF_CONV (value; defCNF)
def_suffix (value; Defn)
default_prover (value; Tactical)
default_termination_simps (value; TotalDefn)
default_WF_thms (value; TotalDefn)
defaultConsumer (value; Portable)
defCNF (structure)
Define (value; TotalDefn, bossLib)
define_case_constant (value; Prim_rec)
define_equivalence_type (value; EquivType)
define_new_type_bijections (value; Drule)
define_type (value; Datatype, ind_types)
DefineSchema (value; TotalDefn)
Definition (constructor; Count)
Definition (structure)
definition (value; DB)
definitions (value; DB)
Defn (structure)
defn (type; Abbrev, DefnBase)
DefnBase (structure)
deinitcomment (value; Lib)
deinitcommentss (value; Lib)
del_consts (value; computeLib)
del_funs (value; computeLib)
del_persistent_consts (value; computeLib)
DELAMB_CONV (value; Canon_Port)
delete (value; Net)
delete_binding (value; Theory)
delete_const (value; Theory, boolSyntax)
DELETE_CONV (value; pred_setLib)
delete_tm (value; pred_setSyntax)
delete_type (value; Theory)
delta (type; Lib)
delta (value; Type)
delta_apply (value; Lib)
delta_map (value; Lib)
delta_pair (value; Lib)
DEPDIR (value; Systeml)
deprecate_int (value; intLib)
deprecate_num (value; numLib)
depth (value; mesonLib)
DEPTH_BINOP_CONV (value; Canon, liteLib)
DEPTH_CONV (value; Conv, liteLib)
DEPTH_EXISTS_CONV (value; unwindLib)
DEPTH_FORALL_CONV (value; unwindLib)
DEPTH_QCONV (value; liteLib)
derive_mono_strong_induction (value; IndDefLib, IndDefRules)
derive_nonschematic_inductive_relations (value; InductiveDefinition)
derive_strong_induction (value; IndDefLib)
DerivedBddRules (structure)
dest (value; Varmap)
dest_abs (value; Psyntax, Rsyntax, Term)
dest_all_distinct (value; listSyntax)
dest_anylet (value; pairSyntax)
dest_app (value; Absyn)
dest_append (value; listLib, listSyntax)
dest_AQ (value; Absyn)
dest_arb (value; boolSyntax)
dest_bag (value; bagLib, bagSyntax)
dest_BddOp (value; DerivedBddRules)
dest_BddOpError (exception; DerivedBddRules)
dest_biginter (value; pred_setSyntax)
dest_bigunion (value; pred_setSyntax)
dest_bij (value; pred_setSyntax)
dest_binder (value; Absyn)
dest_binop (value; liteLib)
dest_bool_case (value; boolSyntax)
DEST_BOUNDED (value; Drule)
dest_C (value; combinSyntax)
dest_card (value; pred_setSyntax)
dest_case (value; TypeBase, TypeBasePure)
dest_choice (value; pred_setSyntax)
dest_chr (value; stringLib, stringSyntax)
dest_cmeasure (value; numSyntax)
dest_comb (value; Psyntax, Rsyntax, Term)
dest_compl (value; pred_setSyntax)
dest_cond (value; Psyntax, Rsyntax, boolSyntax)
dest_conj (value; Absyn, Psyntax, Rsyntax, boolSyntax)
dest_cons (value; listLib, listSyntax)
dest_const (value; Psyntax, Rsyntax, Term)
dest_count (value; pred_setSyntax)
dest_cross (value; pred_setSyntax)
dest_curry (value; pairLib, pairSyntax)
dest_delete (value; pred_setSyntax)
dest_diff (value; bagLib, bagSyntax, pred_setSyntax)
dest_disj (value; Absyn, Psyntax, Rsyntax, boolSyntax)
dest_disjoint (value; pred_setSyntax)
dest_div (value; intSyntax, numSyntax)
dest_divides (value; intSyntax)
dest_divmod (value; numSyntax)
dest_el (value; listLib, listSyntax)
dest_empty (value; pred_setSyntax)
dest_eq (value; Absyn, Psyntax, Rsyntax, boolSyntax)
dest_eq_ty (value; boolSyntax)
dest_even (value; numSyntax)
dest_every (value; listLib, listSyntax)
dest_exists (value; Absyn, Psyntax, Rsyntax, boolSyntax, listLib, listSyntax)
dest_exists1 (value; Absyn, Psyntax, Rsyntax, boolSyntax)
dest_exp (value; numSyntax)
dest_explode (value; stringLib, stringSyntax)
dest_fact (value; numSyntax)
dest_fail (value; combinSyntax)
dest_filter (value; listLib, listSyntax)
dest_finite (value; pred_setSyntax)
dest_flat (value; listLib, listSyntax)
dest_foldl (value; listLib, listSyntax)
dest_foldr (value; listLib, listSyntax)
dest_forall (value; Absyn, Psyntax, Rsyntax, boolSyntax)
dest_front (value; listSyntax)
dest_fst (value; pairLib, pairSyntax)
dest_funpow (value; numSyntax)
dest_geq (value; intSyntax, numSyntax)
dest_great (value; intSyntax)
dest_greater (value; numSyntax)
dest_hd (value; listLib, listSyntax)
dest_I (value; combinSyntax)
dest_ident (value; Absyn)
dest_image (value; pred_setSyntax)
dest_imp (value; Absyn, Psyntax, Rsyntax, boolSyntax, liteLib)
dest_imp_only (value; Psyntax, Rsyntax, boolSyntax)
dest_implode (value; stringLib, stringSyntax)
dest_in (value; pred_setSyntax)
dest_infinite (value; pred_setSyntax)
dest_inj (value; pred_setSyntax)
dest_injected (value; intSyntax)
dest_insert (value; bagLib, bagSyntax, pred_setSyntax)
dest_inter (value; pred_setSyntax)
dest_is_none (value; optionLib, optionSyntax)
dest_is_some (value; optionLib, optionSyntax)
dest_isprefix (value; stringSyntax)
dest_K (value; combinSyntax)
dest_K_1 (value; combinSyntax)
dest_lam (value; Absyn)
dest_last (value; listSyntax)
dest_least (value; numSyntax)
dest_length (value; listLib, listSyntax)
dest_leq (value; intSyntax, numSyntax)
dest_less (value; intSyntax, numSyntax)
dest_let (value; Psyntax, Rsyntax, boolSyntax)
dest_lex (value; pairSyntax)
dest_linv (value; pred_setSyntax)
dest_list (value; listLib, listSyntax)
dest_list_case (value; listSyntax)
dest_list_type (value; listLib, listSyntax)
dest_literal_case (value; boolSyntax)
dest_map (value; listLib, listSyntax)
dest_map2 (value; listLib, listSyntax)
dest_max (value; numSyntax)
dest_max_set (value; pred_setSyntax)
dest_measure (value; numSyntax)
dest_mem (value; listLib, listSyntax)
dest_min (value; numSyntax)
dest_min_set (value; pred_setSyntax)
dest_minus (value; intSyntax, numSyntax)
dest_mod (value; intSyntax, numSyntax)
dest_mult (value; intSyntax, numSyntax)
dest_n2w (value; wordsSyntax)
dest_neg (value; boolSyntax)
dest_negated (value; intSyntax)
dest_nil (value; listLib, listSyntax)
dest_none (value; optionLib, optionSyntax)
dest_null (value; listLib, listSyntax)
dest_num_case (value; numSyntax)
dest_numeral (value; numSyntax)
dest_nzcv (value; wordsSyntax)
dest_o (value; combinSyntax)
dest_odd (value; numSyntax)
dest_option (value; optionLib, optionSyntax)
dest_option_case (value; optionLib, optionSyntax)
dest_option_join (value; optionLib, optionSyntax)
dest_option_map (value; optionLib, optionSyntax)
dest_ord (value; stringLib, stringSyntax)
dest_pabs (value; pairLib, pairSyntax)
dest_pair (value; Absyn, pairLib, pairSyntax)
dest_pair_map (value; pairLib, pairSyntax)
dest_pbinder (value; pairLib, pairSyntax)
dest_pexists (value; pairLib, pairSyntax)
dest_pexists1 (value; pairLib, pairSyntax)
dest_pforall (value; pairLib, pairSyntax)
dest_plet (value; pairSyntax)
dest_plus (value; intSyntax, numSyntax)
dest_pow (value; pred_setSyntax)
dest_pre (value; numSyntax)
dest_prod (value; pairLib, pairSyntax)
dest_pselect (value; pairLib, pairSyntax)
dest_psubset (value; pred_setSyntax)
dest_rat_add (value; ratSyntax)
dest_rat_ainv (value; ratSyntax)
dest_rat_div (value; ratSyntax)
dest_rat_dnm (value; ratSyntax)
dest_rat_geq (value; ratSyntax)
dest_rat_gre (value; ratSyntax)
dest_rat_leq (value; ratSyntax)
dest_rat_les (value; ratSyntax)
dest_rat_minv (value; ratSyntax)
dest_rat_mul (value; ratSyntax)
dest_rat_nmr (value; ratSyntax)
dest_rat_sgn (value; ratSyntax)
dest_rat_sub (value; ratSyntax)
dest_record (value; TypeBase, TypeBasePure)
dest_res_abstract (value; boolSyntax)
dest_res_exists (value; boolSyntax)
dest_res_exists_unique (value; boolSyntax)
dest_res_forall (value; boolSyntax)
dest_res_select (value; boolSyntax)
dest_rest (value; pred_setSyntax)
dest_reverse (value; listSyntax)
dest_rewrites (value; Rewrite)
dest_rinv (value; pred_setSyntax)
dest_S (value; combinSyntax)
dest_select (value; Absyn, Psyntax, Rsyntax, boolSyntax)
dest_set_spec (value; pred_setSyntax)
dest_set_type (value; pred_setSyntax)
dest_sing (value; pred_setSyntax)
dest_snd (value; pairLib, pairSyntax)
dest_some (value; optionLib, optionSyntax)
dest_strcat (value; stringSyntax)
dest_string (value; stringLib, stringSyntax)
dest_string_case (value; stringSyntax)
dest_strlen (value; stringSyntax)
dest_sub_bag (value; bagLib, bagSyntax)
dest_subset (value; pred_setSyntax)
dest_suc (value; numSyntax)
dest_sum (value; listLib, listSyntax, sumSyntax)
dest_sum_image (value; pred_setSyntax)
dest_sum_set (value; pred_setSyntax)
dest_surj (value; pred_setSyntax)
dest_sw2sw (value; wordsSyntax)
dest_tag (value; Tag)
dest_term (value; Psyntax, Rsyntax)
dest_term_bdd (value; PrimitiveBddRules)
dest_the (value; optionLib, optionSyntax)
dest_theory (value; DB)
dest_thm (value; Thm)
dest_thy_const (value; Term)
dest_thy_type (value; Type)
dest_time (value; Portable)
dest_tl (value; listLib, listSyntax)
dest_type (value; Psyntax, Rsyntax, Type)
dest_typed (value; Absyn)
dest_uncurry (value; pairLib, pairSyntax)
dest_union (value; bagLib, bagSyntax, pred_setSyntax)
dest_univ (value; pred_setSyntax)
dest_unzip (value; listLib, listSyntax)
dest_var (value; Psyntax, Rsyntax, Term)
dest_vartype (value; Type)
dest_W (value; combinSyntax)
dest_w2n (value; wordsSyntax)
dest_w2w (value; wordsSyntax)
dest_while (value; numSyntax)
dest_word_1comp (value; wordsSyntax)
dest_word_2comp (value; wordsSyntax)
dest_word_add (value; wordsSyntax)
dest_word_and (value; wordsSyntax)
dest_word_asr (value; wordsSyntax)
dest_word_bit (value; wordsSyntax)
dest_word_bits (value; wordsSyntax)
dest_word_concat (value; wordsSyntax)
dest_word_extract (value; wordsSyntax)
dest_word_ge (value; wordsSyntax)
dest_word_gt (value; wordsSyntax)
dest_word_H (value; wordsSyntax)
dest_word_hi (value; wordsSyntax)
dest_word_hs (value; wordsSyntax)
dest_word_join (value; wordsSyntax)
dest_word_L (value; wordsSyntax)
dest_word_le (value; wordsSyntax)
dest_word_lo (value; wordsSyntax)
dest_word_log2 (value; wordsSyntax)
dest_word_ls (value; wordsSyntax)
dest_word_lsb (value; wordsSyntax)
dest_word_lsl (value; wordsSyntax)
dest_word_lsr (value; wordsSyntax)
dest_word_lt (value; wordsSyntax)
dest_word_modify (value; wordsSyntax)
dest_word_msb (value; wordsSyntax)
dest_word_mul (value; wordsSyntax)
dest_word_or (value; wordsSyntax)
dest_word_reverse (value; wordsSyntax)
dest_word_rol (value; wordsSyntax)
dest_word_ror (value; wordsSyntax)
dest_word_rrx (value; wordsSyntax)
dest_word_slice (value; wordsSyntax)
dest_word_sub (value; wordsSyntax)
dest_word_T (value; wordsSyntax)
dest_word_type (value; wordsSyntax)
dest_word_xor (value; wordsSyntax)
dest_zip (value; listLib, listSyntax)
DIFF (constructor; Lib)
DIFF_CONV (value; realLib)
diff_tm (value; pred_setSyntax)
dim_of (value; wordsSyntax)
disable_tyabbrev_printing (value; Parse)
DISCARD_TAC (value; Tactic)
Disch (constructor; Count)
DISCH (value; Q, Thm)
DISCH_ALL (value; Drule)
DISCH_TAC (value; Tactic)
DISCH_THEN (value; Thm_cont)
Disj1 (constructor; Count)
DISJ1 (value; Q, Thm)
DISJ1_TAC (value; Tactic)
Disj2 (constructor; Count)
DISJ2 (value; Q, Thm)
DISJ2_TAC (value; Tactic)
DISJ_CASES (value; Thm)
DISJ_CASES_TAC (value; Tactic, jrhTactics)
DISJ_CASES_THEN (value; Thm_cont, jrhTactics)
DISJ_CASES_THEN2 (value; Thm_cont)
DISJ_CASES_THENL (value; Thm_cont)
DISJ_CASES_UNION (value; Drule)
DISJ_CASESL (value; Drule)
DISJ_IMP (value; Drule)
DisjCases (constructor; Count)
disjoint_tm (value; pred_setSyntax)
DISJPATH_CONV (value; Canon)
disjunction (value; boolSyntax)
disjuncts (value; hol88Lib)
Disk (constructor; Count)
disk_thm (value; Thm)
distinct_of (value; TypeBase, TypeBasePure)
DISTRIB_CONV (value; AC)
Div (exception; Portable)
div (value; Arbint, Arbnum)
div2 (value; Arbnum)
div2_tm (value; numSyntax)
DIV_CONV (value; reduceLib)
div_tm (value; intSyntax, numSyntax)
divides_tm (value; intSyntax)
divmod (value; Arbint, Arbnum)
divmod_tm (value; numSyntax)
DNF_CONV (value; Canon)
DNF_ss (value; boolSimps)
dom_rng (value; Type)
doms_of_tyaxiom (value; Prim_rec)
dotBdd (value; PrintBdd)
dotLabelledTermBdd (value; PrintBdd)
dotTermBdd (value; PrintBdd)
dotTermBddFlag (value; PrintBdd)
dproc_ss (value; simpLib)
drop (value; goalstackLib)
dropn (value; goalstackLib)
Drule (structure)
DYNLIB (value; Systeml)

E

e (value; goalstackLib)
eager (value; liteLib)
el (value; Lib)
el_tm (value; listLib, listSyntax)
elim_common_factor (value; realSimps)
elim_tcs (value; Defn)
ELIM_TUPLED_QUANT_CONV (value; pairTools)
elts (value; TypeBase)
eltype (value; listLib, listSyntax, pred_setSyntax)
emit_ERR (value; Feedback)
emit_hol_script (value; Systeml)
emit_hol_unquote_script (value; Systeml)
emit_MESG (value; Feedback)
emit_WARNING (value; Feedback)
emitMLDir (value; Globals)
empty (value; Net, TypeBasePure, Varmap)
EMPTY_BAG_tm (value; bagLib, bagSyntax)
empty_model (value; holCheckLib)
empty_net (value; Ho_Net)
empty_rewrites (value; Rewrite)
empty_ss (value; simpLib)
empty_tag (value; Tag)
empty_tm (value; pred_setSyntax)
empty_tmset (value; Term)
empty_varset (value; Term)
emptystring_tm (value; stringLib, stringSyntax)
encode_of (value; TypeBase, TypeBasePure)
encode_of0 (value; TypeBase, TypeBasePure)
end_foldr (value; liteLib)
end_itlist (value; Lib)
end_of_stream (value; Portable)
end_time (value; Lib)
EndInitialBlock (value; Parse)
enter (value; Ho_Net, Net)
enumerate (value; Lib)
eq (value; Preterm, Varmap)
EQ_ABS_CONV (value; Canon)
EQ_IMP_RULE (value; Thm)
EQ_MP (value; Thm)
EQ_TAC (value; Tactic)
EQF_ELIM (value; Drule)
EQF_INTRO (value; Drule)
EqImpRule (constructor; Count)
EqMp (constructor; Count)
eqns_of (value; Defn)
EQT_ELIM (value; Drule)
EQT_INTRO (value; Drule)
eqToTermBdd (value; DerivedBddRules)
equal (value; Lib)
equality (value; boolSyntax)
EquivType (structure)
ERR_outstream (value; Feedback)
ERR_to_string (value; Feedback)
error_record (type; Feedback)
Eta (value; Thm)
ETA_CONV (value; Thm)
eta_conv (value; Term)
ETA_ss (value; boolSimps)
EtaConv (constructor; Count)
etyvar (value; Type)
EVAL (value; bossLib)
eval (value; liteLib)
EVAL_CONV (value; computeLib)
EVAL_RULE (value; bossLib, computeLib)
EVAL_TAC (value; bossLib, computeLib)
EVEN_CONV (value; reduceLib)
even_tm (value; numSyntax)
EVERY (value; Tactical, jrhTactics)
EVERY_ASSUM (value; Tactical)
EVERY_CONJ_CONV (value; Conv)
EVERY_CONV (value; Conv)
EVERY_DISJ_CONV (value; Conv)
EVERY_TCL (value; Thm_cont)
every_tm (value; listLib, listSyntax)
EXISTENCE (value; Conv)
existential (value; boolSyntax)
Exists (constructor; Count)
EXISTS (value; Q, Thm)
exists (value; Lib)
exists1 (value; boolSyntax)
EXISTS_AND_CONV (value; Conv)
EXISTS_AND_REORDER_CONV (value; Conv)
EXISTS_DEL1_CONV (value; unwindLib)
EXISTS_DEL_CONV (value; unwindLib)
EXISTS_EQ (value; Drule)
EXISTS_EQN_CONV (value; unwindLib)
EXISTS_GREATEST_CONV (value; numLib)
EXISTS_IMP (value; Drule)
EXISTS_IMP_CONV (value; Conv)
EXISTS_LEAST_CONV (value; numLib)
EXISTS_NOT_CONV (value; Conv)
EXISTS_OR_CONV (value; Conv)
EXISTS_TAC (value; Q, Tactic)
exists_tm (value; listLib, listSyntax)
exists_tyvar (value; Type)
EXISTS_UNIQUE_CONV (value; Conv)
exit (value; Portable)
exn_to_string (value; Feedback)
EXP_CONV (value; reduceLib)
exp_tm (value; intSyntax, numSyntax)
expand (value; goalstackLib)
EXPAND_ALL_BUT_CONV (value; unwindLib)
EXPAND_ALL_BUT_RIGHT_RULE (value; unwindLib)
EXPAND_AUTO_CONV (value; unwindLib)
EXPAND_AUTO_RIGHT_RULE (value; unwindLib)
expandf (value; goalstackLib)
explode (value; Portable)
explode_tm (value; stringLib, stringSyntax)
export_mono (value; IndDefLib, bossLib)
export_rewrites (value; BasicProvers, bossLib)
export_theorems_as_docfiles (value; Parse)
export_theory (value; Theory)
export_theory_as_docfiles (value; DB)
EXT (value; Drule)
extends (value; Varmap)
extendSat (value; DerivedBddRules)
extendVarmap (value; DerivedBddRules)

F

F (value; boolSyntax)
fact_tm (value; numSyntax)
FAIL (constructor; Lib)
fail (exception; DerivedBddRules)
fail (value; Feedback, liteLib)
FAIL_TAC (value; Tactical)
fail_tm (value; combinSyntax)
failfn (value; DerivedBddRules)
failwith (value; Feedback, liteLib)
FCP_ss (value; fcpLib)
fcpLib (structure)
Feedback (structure)
fetch (value; DB, TypeBase, TypeBasePure)
field_name (type; Datatype)
field_names (type; Datatype)
fields_of (value; TypeBase, TypeBasePure)
filter (value; Lib, Net)
FILTER_ASM_REWRITE_RULE (value; Ho_Rewrite, Rewrite)
FILTER_ASM_REWRITE_TAC (value; Ho_Rewrite, Rewrite)
FILTER_DISCH_TAC (value; Tactic)
FILTER_DISCH_THEN (value; Tactic)
FILTER_GEN_TAC (value; Tactic)
FILTER_ONCE_ASM_REWRITE_RULE (value; Ho_Rewrite, Rewrite)
FILTER_ONCE_ASM_REWRITE_TAC (value; Ho_Rewrite, Rewrite)
FILTER_PGEN_TAC (value; PairRules)
FILTER_PSTRIP_TAC (value; PairRules)
FILTER_PSTRIP_THEN (value; PairRules)
FILTER_PURE_ASM_REWRITE_RULE (value; Ho_Rewrite, Rewrite)
FILTER_PURE_ASM_REWRITE_TAC (value; Ho_Rewrite, Rewrite)
FILTER_PURE_ONCE_ASM_REWRITE_RULE (value; Ho_Rewrite, Rewrite)
FILTER_PURE_ONCE_ASM_REWRITE_TAC (value; Ho_Rewrite, Rewrite)
FILTER_STRIP_TAC (value; Tactic)
FILTER_STRIP_THEN (value; Tactic)
filter_tm (value; listLib, listSyntax)
find (value; DB, hol88Lib)
findModel (value; DerivedBddRules)
findModelError (exception; DerivedBddRules)
findTrace (value; DerivedBddRules)
FINITE_CONV (value; pred_setLib)
finite_tm (value; pred_setSyntax)
FIRST (value; Tactical)
first (value; Lib)
FIRST_ASSUM (value; Tactical, jrhTactics)
FIRST_CONV (value; Conv)
FIRST_PROVE (value; Tactical)
FIRST_TCL (value; Thm_cont)
FIRST_X_ASSUM (value; Tactical, jrhTactics)
fixity (type; Parse)
fixity (value; Parse)
flat (value; hol88Lib)
flat_tm (value; listLib, listSyntax)
flatten (value; Lib)
FLATTEN_CONJ_CONV (value; unwindLib)
flatten_pair (value; DerivedBddRules)
flip_order (value; Lib)
floor (value; Arbnum)
flush_out (value; Portable)
FOL_CONV (value; Canon)
foldl (value; liteLib)
foldl_tm (value; listLib, listSyntax)
foldr (value; liteLib)
foldr_tm (value; listLib, listSyntax)
for (value; Lib)
for_se (value; Lib)
forall (value; hol88Lib)
FORALL_AND_CONV (value; Conv)
FORALL_CONJ_CONV (value; unwindLib)
FORALL_CONJ_ONCE_CONV (value; unwindLib)
FORALL_CONJ_RIGHT_RULE (value; unwindLib)
FORALL_EQ (value; Drule)
FORALL_IMP_CONV (value; Conv)
FORALL_NOT_CONV (value; Conv)
FORALL_OR_CONV (value; Conv)
FORK_CONV (value; Conv)
format_ERR (value; Feedback)
format_MESG (value; Feedback)
format_WARNING (value; Feedback)
frag (type; Lib, Parse, Portable)
free_in (value; Term)
free_vars (value; Term)
free_vars_lr (value; Term)
free_varsl (value; Term)
frees (value; hol88Lib)
freesl (value; Canon_Port, hol88Lib)
FREEZE_THEN (value; Tactic)
fromBinString (value; Arbnum)
fromHexString (value; Arbnum)
fromHOLchar (value; stringLib, stringSyntax)
fromHOLstring (value; stringLib, stringSyntax)
fromInt (value; Arbint, Arbnum)
fromMLchar (value; stringLib, stringSyntax)
fromMLstring (value; stringLib, stringSyntax)
fromNat (value; Arbint)
fromOctString (value; Arbnum)
fromString (value; Arbint, Arbnum)
FRONT_CONJ_CONV (value; Drule)
front_last (value; Lib)
front_tm (value; listSyntax)
fst (value; Lib)
fst_tm (value; pairLib, pairSyntax)
ftyvar (value; Type)
FULL_SIMP_TAC (value; bossLib, simpLib)
FULL_STRUCT_CASES_TAC (value; Tactic)
FUN_EQ_CONV (value; Conv)
funpow (value; Lib)
funpow_tm (value; numSyntax)
FVL (value; Term)

G

g (value; goalstackLib)
gamma (value; Type)
gather (value; Lib)
gcd (value; Arbnum)
GE_CONV (value; reduceLib)
Gen (constructor; Count)
GEN (value; Q, Thm)
GEN_ABS (value; Thm)
GEN_ALL (value; Drule, hol88Lib)
gen_all (value; boolSyntax)
GEN_ALPHA_CONV (value; Drule)
GEN_BETA_CONV (value; PairedLambda, pairLib)
GEN_BETA_RULE (value; PairedLambda, pairLib)
GEN_BETA_TAC (value; PairedLambda, pairLib)
GEN_COND_CASES_TAC (value; Tactic)
gen_datatype_info (value; TypeBasePure)
GEN_FOL_CONV (value; Canon_Port)
GEN_MESON_TAC (value; mesonLib)
GEN_PALPHA_CONV (value; PairRules)
GEN_PROVE_TAC (value; BasicProvers)
GEN_REWRITE_CONV (value; Ho_Rewrite, Rewrite)
GEN_REWRITE_RULE (value; Ho_Rewrite, Rewrite, hol88Lib)
GEN_REWRITE_TAC (value; Ho_Rewrite, Rewrite, hol88Lib)
GEN_TAC (value; Tactic)
gen_tyvar (value; Type)
gen_variant (value; Lexis)
gen_wfrec_definition (value; Defn)
GenAbs (constructor; Count)
genFromString (value; Arbnum)
GENL (value; Thm)
GenTermToTermBdd (value; DerivedBddRules)
genvar (value; Term)
genvars (value; Term)
genvarstruct (value; pairLib, pairSyntax)
geq_tm (value; intSyntax, numSyntax)
get (value; TypeBasePure)
get_flag_abs (value; holCheckLib)
get_flag_ric (value; holCheckLib)
get_init (value; holCheckLib)
get_name (value; holCheckLib)
get_props (value; holCheckLib)
get_results (value; holCheckLib)
get_state (value; holCheckLib)
get_term_printer (value; Parse)
get_thm_heads (value; Canon_Port)
get_tracefn (value; Feedback)
get_trans (value; holCheckLib)
get_vord (value; holCheckLib)
getArgs (value; Portable)
getAssums (value; PrimitiveBddRules)
getBdd (value; PrimitiveBddRules)
getEnv (value; Portable)
getTag (value; PrimitiveBddRules)
getTerm (value; PrimitiveBddRules)
getVarmap (value; PrimitiveBddRules)
give_num_priority (value; Parse)
global_varmap (value; DerivedBddRules)
Globals (structure)
GNUMAKE (value; Systeml)
Goal (type; jrhTactics)
goal (type; Abbrev, ratLib)
goal_line (value; Globals)
goalstack (type; goalstackLib)
goalstackLib (structure)
Goalstate (type; jrhTactics)
GPSPEC (value; PairRules)
great_tm (value; intSyntax)
greater_tm (value; numSyntax)
GSPEC (value; Drule)
gspec_tm (value; pred_setSyntax)
GSUBS (value; Drule)
GSUBST_TAC (value; Tactic)
GSYM (value; Conv)
GT_CONV (value; reduceLib)
guessing_overloads (value; Globals)
guessing_tyvars (value; Globals)
guessR (value; TotalDefn)

H

HALF_MK_PABS (value; PairRules)
HardSpace (value; Parse)
hash (value; Lib)
hd_tm (value; listLib, listSyntax)
hidden (value; Parse)
hide (value; Parse)
HIGHER_REWRITE_CONV (value; Ho_Rewrite)
HO_BACKCHAIN_TAC (value; Tactic)
HO_MATCH_ABBREV_TAC (value; Q)
HO_MATCH_ACCEPT_TAC (value; Tactic)
HO_MATCH_MP (value; Drule)
HO_MATCH_MP_TAC (value; Tactic)
Ho_Net (structure)
HO_PART_MATCH (value; Drule)
HO_REWR_CONV (value; Conv)
Ho_Rewrite (structure)
hol88Lib (structure)
hol88subst (type; hol88Lib)
hol88subst_of (value; hol88Lib)
hol_clock (value; Globals)
Hol_datatype (value; Datatype, bossLib)
Hol_defn (value; Defn, bossLib)
HOL_ERR (exception; Feedback)
HOL_MESG (value; Feedback)
Hol_mono_reln (value; IndDefLib)
Hol_pp (structure)
HOL_PROGRESS_MESG (value; Feedback)
Hol_Rdefn (value; Defn)
Hol_reln (value; IndDefLib, bossLib)
hol_symbols (value; Lexis)
hol_type (type; Abbrev, Hol_pp, Parse, Preterm, Psyntax, Rsyntax, Term, Theory, Thm, Type, TypeBase, TypeBasePure, boolSyntax, ratSyntax)
HOL_WARNING (value; Feedback)
HOL_WARNINGloc (value; Feedback)
holCheck (value; holCheckLib)
holCheckLib (structure)
HOLDIR (value; Globals, Systeml)
HolSatLib (structure)
html_theory (value; DB)
hyp (value; Thm)
hyp_frees (value; Thm)
hyp_tyvars (value; Thm)
hypset (value; Thm)

I

I (value; Lib)
I_tm (value; combinSyntax)
ID_EX_TAC (value; Q)
ID_SPEC (value; Q)
ID_SPEC_TAC (value; Q, Tactic)
idem_tm (value; boolSyntax)
IDENT (constructor; Absyn)
IF_CASES_TAC (value; Tactic)
IMAGE_CONV (value; pred_setLib)
image_tm (value; pred_setSyntax)
IMP_ANTISYM_RULE (value; Drule)
IMP_CANON (value; Drule)
IMP_CONJ (value; Drule)
IMP_CONV (value; reduceLib)
IMP_ELIM (value; Drule)
IMP_RES_TAC (value; Tactic)
IMP_RES_THEN (value; Thm_cont)
IMP_TRANS (value; Drule)
implication (value; boolSyntax)
implicit_rewrites (value; Ho_Rewrite, Rewrite)
implode (value; Portable)
implode_tm (value; stringLib, stringSyntax)
in_class (value; Lexis)
IN_CONV (value; pred_setLib)
in_tm (value; pred_setSyntax)
inc (value; Portable)
inc_count (value; Count)
incorporate_consts (value; Theory)
incorporate_types (value; Theory)
ind (value; Type)
ind_of (value; Defn)
ind_suffix (value; Defn)
ind_types (structure)
IndDefLib (structure)
IndDefRules (structure)
index (value; Lib, Net)
Induct (value; SingleStep, bossLib)
Induct_on (value; SingleStep, bossLib)
INDUCT_TAC (value; numLib)
INDUCT_THEN (value; Prim_rec)
induction_of (value; TypeBase, TypeBasePure)
induction_of0 (value; TypeBase, TypeBasePure)
InductiveDefinition (structure)
infinite_tm (value; pred_setSyntax)
Infix (value; Parse)
Infixl (value; Parse)
Infixr (value; Parse)
initial_goal (value; goalstackLib)
inj_tm (value; pred_setSyntax)
INL (constructor; sumSyntax)
inl_tm (value; sumSyntax)
input_line (value; Portable)
INR (constructor; sumSyntax)
inr_tm (value; sumSyntax)
insert (value; Lib, Net, TypeBasePure, Varmap)
INSERT_CONV (value; pred_setLib)
insert_tm (value; pred_setSyntax)
Inst (constructor; Count)
INST (value; Q, Thm, hol88Lib)
inst (value; Term, hol88Lib)
inst_defn (value; Defn)
INST_TY_TERM (value; Drule, hol88Lib)
INST_TYPE (value; Q, Thm, hol88Lib)
inst_type (value; hol88Lib)
instream (type; Portable)
InstType (constructor; Count)
inSupport (value; PrimitiveBddRules)
int (type; Arbint)
int_eq_tm (value; intSyntax)
int_injection (value; intSyntax)
INT_NORM_CONV (value; integerRingLib)
INT_NORM_RULE (value; integerRingLib)
INT_NORM_TAC (value; integerRingLib)
int_of_string (value; hol88Lib)
int_of_term (value; intSyntax, numSyntax)
int_rewrites (value; ratLib)
INT_RING_CONV (value; integerRingLib)
INT_RING_RULE (value; integerRingLib)
INT_RING_TAC (value; integerRingLib)
int_sort (value; Lib)
int_ss (value; intLib)
int_to_string (value; Lib)
int_ty (value; intSyntax)
integerRingLib (structure)
inter_tm (value; pred_setSyntax)
interactive (value; Globals)
Interrupt (exception; Portable)
intersect (value; Lib)
intLib (structure)
intSyntax (structure)
intToTerm (value; DerivedBddRules)
inv_img_cmp (value; Lib)
Io (exception; Portable)
IPSPEC (value; PairRules)
IPSPECL (value; PairRules)
is_abs (value; Term)
is_absval (value; intSyntax)
is_all_distinct (value; listSyntax)
is_app (value; Absyn)
is_append (value; listLib, listSyntax)
is_AQ (value; Absyn)
is_arb (value; boolSyntax)
is_arith (value; numSimps)
is_arith_asm (value; numSimps)
is_bag_ty (value; bagLib, bagSyntax)
is_biginter (value; pred_setSyntax)
is_bigunion (value; pred_setSyntax)
is_bij (value; pred_setSyntax)
is_binop (value; liteLib)
is_bool_case (value; boolSyntax)
is_C (value; combinSyntax)
is_card (value; pred_setSyntax)
is_case (value; TypeBase, TypeBasePure)
is_char_literal (value; Lexis)
is_choice (value; pred_setSyntax)
is_chr (value; stringLib, stringSyntax)
is_comb (value; Term)
is_compl (value; pred_setSyntax)
is_cond (value; boolSyntax)
is_conj (value; Absyn, boolSyntax)
is_cons (value; listLib, listSyntax)
is_const (value; Term)
is_constructor (value; TypeBase, TypeBasePure)
is_count (value; pred_setSyntax)
is_cross (value; pred_setSyntax)
is_curry (value; pairLib, pairSyntax)
is_delete (value; pred_setSyntax)
is_diff (value; bagLib, bagSyntax, pred_setSyntax)
is_disj (value; Absyn, boolSyntax)
is_disjoint (value; pred_setSyntax)
is_div (value; intSyntax, numSyntax)
is_divides (value; intSyntax)
is_divmod (value; numSyntax)
is_el (value; listLib, listSyntax)
is_empty (value; pred_setSyntax)
is_emptystring (value; stringLib, stringSyntax)
is_eq (value; Absyn, boolSyntax)
is_eqc (value; Canon_Port)
is_even (value; numSyntax)
is_every (value; listLib, listSyntax)
is_exists (value; Absyn, boolSyntax, listLib, listSyntax)
is_exists1 (value; Absyn, boolSyntax)
is_exp (value; numSyntax)
is_explode (value; stringLib, stringSyntax)
is_fact (value; numSyntax)
is_fail (value; combinSyntax)
is_filter (value; listLib, listSyntax)
is_finite (value; pred_setSyntax)
is_flat (value; listLib, listSyntax)
is_foldl (value; listLib, listSyntax)
is_foldr (value; listLib, listSyntax)
is_forall (value; Absyn, boolSyntax)
is_front (value; listSyntax)
is_fst (value; pairLib, pairSyntax)
is_funpow (value; numSyntax)
is_gen_tyvar (value; Type)
is_genvar (value; Term)
is_geq (value; intSyntax, numSyntax)
is_great (value; intSyntax)
is_greater (value; numSyntax)
is_hd (value; listLib, listSyntax)
is_I (value; combinSyntax)
is_ident (value; Absyn)
is_image (value; pred_setSyntax)
is_imp (value; Absyn, boolSyntax, liteLib)
is_imp_only (value; boolSyntax)
is_implode (value; stringLib, stringSyntax)
is_in (value; pred_setSyntax)
is_infinite (value; pred_setSyntax)
is_inj (value; pred_setSyntax)
is_injected (value; intSyntax)
is_insert (value; bagLib, bagSyntax, pred_setSyntax)
is_int_literal (value; intSyntax)
is_inter (value; pred_setSyntax)
is_is_none (value; optionLib, optionSyntax)
is_is_some (value; optionLib, optionSyntax)
is_isprefix (value; stringSyntax)
is_K (value; combinSyntax)
is_K_1 (value; combinSyntax)
is_lam (value; Absyn)
is_last (value; listSyntax)
is_least (value; numSyntax)
is_length (value; listLib, listSyntax)
is_leq (value; intSyntax, numSyntax)
is_less (value; intSyntax, numSyntax)
is_let (value; boolSyntax)
is_lex (value; pairSyntax)
is_linv (value; pred_setSyntax)
is_list (value; listLib, listSyntax)
is_list_case (value; listSyntax)
is_list_type (value; listLib, listSyntax)
is_literal_case (value; boolSyntax)
is_map (value; listLib, listSyntax)
is_map2 (value; listLib, listSyntax)
is_max (value; numSyntax)
is_max_set (value; pred_setSyntax)
is_measure (value; numSyntax)
is_mem (value; listLib, listSyntax)
is_min (value; numSyntax)
is_min_set (value; pred_setSyntax)
is_minus (value; intSyntax, numSyntax)
is_mod (value; intSyntax, numSyntax)
is_mult (value; intSyntax, numSyntax)
is_n2w (value; wordsSyntax)
is_neg (value; boolSyntax)
is_negated (value; intSyntax)
is_nil (value; listLib, listSyntax)
is_none (value; liteLib, optionLib, optionSyntax)
is_none_tm (value; optionLib, optionSyntax)
is_null (value; listLib, listSyntax)
is_num_case (value; numSyntax)
is_num_literal (value; Lexis)
is_numeral (value; numSyntax)
is_nzcv (value; wordsSyntax)
is_o (value; combinSyntax)
is_odd (value; numSyntax)
is_option (value; optionLib, optionSyntax)
is_option_case (value; optionLib, optionSyntax)
is_option_join (value; optionLib, optionSyntax)
is_option_map (value; optionLib, optionSyntax)
is_ord (value; stringLib, stringSyntax)
is_pabs (value; pairLib, pairSyntax)
is_pair (value; Absyn, pairLib, pairSyntax)
is_pair_map (value; pairLib, pairSyntax)
is_pexists (value; pairLib, pairSyntax)
is_pexists1 (value; pairLib, pairSyntax)
is_pforall (value; pairLib, pairSyntax)
is_plet (value; pairSyntax)
is_plus (value; intSyntax, numSyntax)
is_pow (value; pred_setSyntax)
is_pre (value; numSyntax)
is_presburger (value; Cooper)
is_pselect (value; pairLib, pairSyntax)
is_psubset (value; pred_setSyntax)
is_rat_add (value; ratSyntax)
is_rat_ainv (value; ratSyntax)
is_rat_div (value; ratSyntax)
is_rat_dnm (value; ratSyntax)
is_rat_geq (value; ratSyntax)
is_rat_gre (value; ratSyntax)
is_rat_leq (value; ratSyntax)
is_rat_les (value; ratSyntax)
is_rat_minv (value; ratSyntax)
is_rat_mul (value; ratSyntax)
is_rat_nmr (value; ratSyntax)
is_rat_sgn (value; ratSyntax)
is_rat_sub (value; ratSyntax)
is_record (value; TypeBase, TypeBasePure)
is_res_abstract (value; boolSyntax)
is_res_exists (value; boolSyntax)
is_res_exists_unique (value; boolSyntax)
is_res_forall (value; boolSyntax)
is_res_select (value; boolSyntax)
is_rest (value; pred_setSyntax)
is_reverse (value; listSyntax)
is_rinv (value; pred_setSyntax)
is_S (value; combinSyntax)
is_select (value; Absyn, boolSyntax)
is_set_spec (value; pred_setSyntax)
is_set_type (value; pred_setSyntax)
is_sing (value; pred_setSyntax)
is_snd (value; pairLib, pairSyntax)
is_some (value; liteLib, optionLib, optionSyntax)
is_some_tm (value; optionLib, optionSyntax)
is_strcat (value; stringSyntax)
is_string (value; stringLib, stringSyntax)
is_string_case (value; stringSyntax)
is_string_literal (value; Lexis, stringSyntax)
is_strlen (value; stringSyntax)
is_sub_bag (value; bagLib, bagSyntax)
is_subset (value; pred_setSyntax)
is_substring (value; Lib)
is_suc (value; numSyntax)
is_sum (value; listLib, listSyntax)
is_sum_image (value; pred_setSyntax)
is_sum_set (value; pred_setSyntax)
is_surj (value; pred_setSyntax)
is_sw2sw (value; wordsSyntax)
is_the (value; optionLib, optionSyntax)
is_the_value (value; boolSyntax)
is_tl (value; listLib, listSyntax)
is_type (value; Type)
is_typed (value; Absyn)
is_uncurry (value; pairLib, pairSyntax)
is_union (value; bagLib, bagSyntax, pred_setSyntax)
is_univ (value; pred_setSyntax)
is_unzip (value; listLib, listSyntax)
is_var (value; Term)
is_vartype (value; Type)
is_vstruct (value; pairLib, pairSyntax)
is_W (value; combinSyntax)
is_w2n (value; wordsSyntax)
is_w2w (value; wordsSyntax)
is_while (value; numSyntax)
is_word_1comp (value; wordsSyntax)
is_word_2comp (value; wordsSyntax)
is_word_add (value; wordsSyntax)
is_word_and (value; wordsSyntax)
is_word_asr (value; wordsSyntax)
is_word_bit (value; wordsSyntax)
is_word_bits (value; wordsSyntax)
is_word_concat (value; wordsSyntax)
is_word_extract (value; wordsSyntax)
is_word_ge (value; wordsSyntax)
is_word_gt (value; wordsSyntax)
is_word_H (value; wordsSyntax)
is_word_hi (value; wordsSyntax)
is_word_hs (value; wordsSyntax)
is_word_L (value; wordsSyntax)
is_word_le (value; wordsSyntax)
is_word_lo (value; wordsSyntax)
is_word_log2 (value; wordsSyntax)
is_word_ls (value; wordsSyntax)
is_word_lsb (value; wordsSyntax)
is_word_lsl (value; wordsSyntax)
is_word_lsr (value; wordsSyntax)
is_word_lt (value; wordsSyntax)
is_word_modify (value; wordsSyntax)
is_word_msb (value; wordsSyntax)
is_word_mul (value; wordsSyntax)
is_word_or (value; wordsSyntax)
is_word_reverse (value; wordsSyntax)
is_word_rol (value; wordsSyntax)
is_word_ror (value; wordsSyntax)
is_word_rrx (value; wordsSyntax)
is_word_slice (value; wordsSyntax)
is_word_sub (value; wordsSyntax)
is_word_T (value; wordsSyntax)
is_word_type (value; wordsSyntax)
is_word_xor (value; wordsSyntax)
is_zip (value; listLib, listSyntax)
isDisk (value; Tag)
isEmpty (value; Tag)
isFALSE (value; DerivedBddRules)
isl_tm (value; sumSyntax)
ISPEC (value; Drule, Q)
ISPEC_THEN (value; Q)
ISPECL (value; Drule, Q)
ISPECL_THEN (value; Q)
isprefix_tm (value; stringSyntax)
isr_tm (value; sumSyntax)
istream (type; Lib)
isTRUE (value; DerivedBddRules)
isUnix (value; Systeml)
iterate (value; DerivedBddRules)
itlist (value; Lib)
itlist2 (value; Lib)
itnet (value; Net)
itotal (value; Lib)

J

jrhTactics (structure)

K

K (value; Lib)
K_tm (value; combinSyntax)
KI (value; hol88Lib)
KNOW_TAC (value; Tactic)
known_constants (value; Parse)

L

LAM (constructor; Absyn)
LAMB (constructor; Psyntax, Rsyntax)
lambda (type; Psyntax, Rsyntax)
LAND_CONV (value; Conv, liteLib)
last (value; Lib)
LAST_EXISTS_CONV (value; Conv)
LAST_FORALL_CONV (value; Conv)
last_tm (value; listSyntax)
latest (value; Canon)
lazy (type; liteLib)
lazy (value; liteLib)
lazyfy_thm (value; computeLib)
ldistrib_tm (value; boolSyntax)
LE_CONV (value; reduceLib)
LEAST_ELIM_TAC (value; numLib)
least_tm (value; numSyntax)
LEAVE_LETS (value; BasicProvers)
LEFT (value; Parse)
LEFT_AND_EXISTS_CONV (value; Conv)
LEFT_AND_FORALL_CONV (value; Conv)
LEFT_AND_PEXISTS_CONV (value; PairRules)
LEFT_AND_PFORALL_CONV (value; PairRules)
LEFT_IMP_EXISTS_CONV (value; Conv)
LEFT_IMP_FORALL_CONV (value; Conv)
LEFT_IMP_PEXISTS_CONV (value; PairRules)
LEFT_IMP_PFORALL_CONV (value; PairRules)
LEFT_LIST_PBETA (value; PairRules)
LEFT_OR_EXISTS_CONV (value; Conv)
LEFT_OR_FORALL_CONV (value; Conv)
LEFT_OR_PEXISTS_CONV (value; PairRules)
LEFT_OR_PFORALL_CONV (value; PairRules)
LEFT_PBETA (value; PairRules)
length_tm (value; listLib, listSyntax)
leq_tm (value; intSyntax, numSyntax)
less1 (value; Arbnum)
less2 (value; Arbnum)
less_tm (value; intSyntax, numSyntax)
let_CONV (value; PairedLambda, pairLib)
LET_ELIM_TAC (value; BasicProvers)
LET_EQ_TAC (value; pairLib, pairTools)
LET_INTRO (value; pairLib, pairTools)
LET_INTRO_TAC (value; pairLib, pairTools)
LET_ss (value; boolSimps)
let_tm (value; boolSyntax)
lex_tm (value; pairSyntax)
Lexis (structure)
lhand (value; liteLib)
lhs (value; boolSyntax)
LHS_CONV (value; Conv)
Lib (structure)
lift_bool (value; boolSyntax)
lift_char (value; stringSyntax)
LIFT_COND_ss (value; boolSimps)
lift_list (value; listSyntax)
lift_num (value; numSyntax)
lift_of (value; TypeBasePure)
lift_option (value; optionSyntax)
lift_prod (value; pairSyntax)
lift_string (value; stringSyntax)
lift_sum (value; sumSyntax)
line_name (value; unwindLib)
line_var (value; unwindLib)
linewidth (value; Globals)
link_parents (value; Theory)
linv_tm (value; pred_setSyntax)
LIST_BETA_CONV (value; Drule)
list_case_tm (value; listSyntax)
list_compare (value; Lib)
LIST_CONJ (value; Drule)
list_mk_abs (value; Term, boolSyntax)
list_mk_anylet (value; pairSyntax)
list_mk_app (value; Absyn)
list_mk_biginter (value; pred_setSyntax)
list_mk_bigunion (value; pred_setSyntax)
list_mk_binder (value; Term)
list_mk_comb (value; Term)
list_mk_conj (value; Absyn, boolSyntax)
list_mk_disj (value; Absyn, boolSyntax)
LIST_MK_EXISTS (value; Drule)
list_mk_exists (value; Absyn, boolSyntax)
list_mk_exists1 (value; Absyn)
list_mk_forall (value; Absyn, boolSyntax)
list_mk_fun (value; boolSyntax)
list_mk_icomb (value; liteLib)
list_mk_imp (value; Absyn, boolSyntax)
list_mk_insert (value; bagLib, bagSyntax)
list_mk_lam (value; Absyn)
list_mk_mult (value; intSyntax, numSyntax)
list_mk_pabs (value; pairLib, pairSyntax)
list_mk_pair (value; Absyn, pairLib, pairSyntax)
LIST_MK_PEXISTS (value; PairRules)
list_mk_pexists (value; pairLib, pairSyntax)
LIST_MK_PFORALL (value; PairRules)
list_mk_pforall (value; pairLib, pairSyntax)
list_mk_plus (value; intSyntax, numSyntax)
list_mk_prod (value; pairLib, pairSyntax)
list_mk_res_exists (value; boolSyntax)
list_mk_res_forall (value; boolSyntax)
list_mk_select (value; Absyn)
list_mk_sum (value; sumSyntax)
list_mk_union (value; bagLib, bagSyntax)
LIST_MP (value; Drule)
list_ord (value; liteLib)
LIST_PBETA_CONV (value; PairRules)
list_rat_add (value; ratSyntax)
list_rat_mul (value; ratSyntax)
list_rws (value; listSimps)
LIST_ss (value; listSimps)
list_ss (value; bossLib)
listDB (value; DB)
listDir (value; Portable)
listItems (value; Net, TypeBasePure)
listLib (structure)
listSimps (structure)
listSyntax (structure)
liteLib (structure)
literal_case (value; boolSyntax)
literal_case_ss (value; boolSimps)
locn (value; Preterm)
locn_of_absyn (value; Absyn)
locn_of_vstruct (value; Absyn)
log2 (value; Arbnum)
lookup (value; Ho_Net, Net)
LT_CONV (value; reduceLib)
lt_of_ord (value; liteLib)
LTL2OMEGA_CONV (value; temporalLib)
LTL_CONV (value; temporalLib)

M

make_log_file (value; Systeml)
MakeSimpRecThm (value; DerivedBddRules)
map (value; Net)
map2 (value; Lib)
map2_tm (value; listLib, listSyntax)
MAP_EVERY (value; Tactical, jrhTactics)
MAP_FIRST (value; Tactical)
map_tm (value; listLib, listSyntax)
mapfilter (value; Lib)
match (value; DB, Net, hol88Lib)
MATCH_ABBREV_TAC (value; Q)
MATCH_ACCEPT_TAC (value; Tactic)
MATCH_MP (value; Drule)
MATCH_MP_TAC (value; Tactic)
match_term (value; Term, hol88Lib)
match_terml (value; Term)
match_type (value; Type, hol88Lib)
match_type_in_context (value; Type)
match_type_restr (value; Type)
matcher (value; DB)
matchp (value; DB)
max (value; Arbint)
max_depth (value; mesonLib)
max_print_depth (value; Globals)
max_set_tm (value; pred_setSyntax)
max_tm (value; intSyntax, numSyntax)
measure_cmp (value; Lib)
measure_tm (value; numSyntax)
measureInduct_on (value; SingleStep, bossLib)
mem (value; Lib)
mem_tm (value; listLib, listSyntax)
merge (value; Tag)
merge_nets (value; Ho_Net)
merge_ss (value; simpLib)
MESG_outstream (value; Feedback)
MESG_to_string (value; Feedback)
MESON_TAC (value; mesonLib)
mesonLib (structure)
meter (type; Count)
METIS_PROVE (value; bossLib)
METIS_TAC (value; bossLib)
min (value; Arbint)
min_grammars (value; Parse)
min_set_tm (value; pred_setSyntax)
min_tm (value; intSyntax, numSyntax)
minisatp (value; HolSatLib)
minus_tm (value; intSyntax, numSyntax)
MK_ABS (value; Drule)
Mk_abs (value; Thm)
mk_abs (value; Psyntax, Rsyntax, Term)
MK_ABS_CONV (value; liteLib)
MK_ABSL_CONV (value; liteLib)
mk_absval (value; intSyntax)
MK_AC_LCOMM (value; Drule)
mk_all_distinct (value; listSyntax)
mk_anylet (value; pairSyntax)
mk_app (value; Absyn)
mk_append (value; listLib, listSyntax)
mk_AQ (value; Absyn)
mk_arb (value; boolSyntax)
mk_bag (value; bagLib, bagSyntax)
mk_biginter (value; pred_setSyntax)
mk_bigunion (value; pred_setSyntax)
mk_bij (value; pred_setSyntax)
mk_binder (value; Absyn)
MK_BINOP (value; liteLib)
mk_binop (value; liteLib)
mk_bool_case (value; boolSyntax)
MK_BOUNDED (value; Drule)
mk_C (value; combinSyntax)
mk_card (value; pred_setSyntax)
mk_case (value; TypeBase, TypeBasePure)
mk_choice (value; pred_setSyntax)
mk_chr (value; stringLib, stringSyntax)
mk_cmeasure (value; numSyntax)
MK_COMB (value; Thm)
Mk_comb (value; Thm)
mk_comb (value; Psyntax, Rsyntax, Term)
MK_COMB_TAC (value; Tactic)
mk_compl (value; pred_setSyntax)
mk_cond (value; Psyntax, Rsyntax, boolSyntax)
MK_CONJ (value; liteLib)
mk_conj (value; Absyn, Psyntax, Rsyntax, boolSyntax)
mk_cons (value; listLib, listSyntax)
mk_const (value; Psyntax, Rsyntax, Term)
mk_consumer (value; Portable)
mk_count (value; pred_setSyntax)
mk_cross (value; pred_setSyntax)
mk_curry (value; pairLib, pairSyntax)
mk_datatype_info (value; TypeBasePure)
mk_defn (value; Defn)
mk_delete (value; pred_setSyntax)
mk_diff (value; bagLib, bagSyntax, pred_setSyntax)
MK_DISJ (value; liteLib)
mk_disj (value; Absyn, Psyntax, Rsyntax, boolSyntax)
mk_disjoint (value; pred_setSyntax)
mk_div (value; intSyntax, numSyntax)
mk_divides (value; intSyntax)
mk_divmod (value; numSyntax)
mk_el (value; listLib, listSyntax)
mk_empty (value; pred_setSyntax)
mk_eq (value; Absyn, Psyntax, Rsyntax, boolSyntax)
mk_even (value; numSyntax)
mk_every (value; listLib, listSyntax)
MK_EXISTS (value; Drule, liteLib)
mk_exists (value; Absyn, Psyntax, Rsyntax, boolSyntax, listLib, listSyntax)
mk_exists1 (value; Absyn, Psyntax, Rsyntax, boolSyntax)
mk_exp (value; numSyntax)
mk_explode (value; stringLib, stringSyntax)
mk_fact (value; numSyntax)
mk_fail (value; combinSyntax)
mk_filter (value; listLib, listSyntax)
mk_finite (value; pred_setSyntax)
mk_flat (value; listLib, listSyntax)
mk_foldl (value; listLib, listSyntax)
mk_foldr (value; listLib, listSyntax)
MK_FORALL (value; liteLib)
mk_forall (value; Absyn, Psyntax, Rsyntax, boolSyntax)
mk_front (value; listSyntax)
mk_fst (value; pairLib, pairSyntax)
mk_funpow (value; numSyntax)
mk_geq (value; intSyntax, numSyntax)
mk_Goalstate (value; jrhTactics)
mk_great (value; intSyntax)
mk_greater (value; numSyntax)
mk_hd (value; listLib, listSyntax)
mk_HOL_ERR (value; Feedback)
mk_HOL_ERRloc (value; Feedback)
mk_I (value; combinSyntax)
mk_icomb (value; liteLib)
mk_ident (value; Absyn)
mk_image (value; pred_setSyntax)
mk_imp (value; Absyn, Psyntax, Rsyntax, boolSyntax)
mk_implode (value; stringLib, stringSyntax)
mk_in (value; pred_setSyntax)
mk_index_size (value; wordsLib)
mk_index_type (value; fcpLib)
mk_infinite (value; pred_setSyntax)
mk_inj (value; pred_setSyntax)
mk_injected (value; intSyntax)
mk_inl (value; sumSyntax)
mk_inr (value; sumSyntax)
mk_insert (value; bagLib, bagSyntax, pred_setSyntax)
mk_inter (value; pred_setSyntax)
mk_is_none (value; optionLib, optionSyntax)
mk_is_some (value; optionLib, optionSyntax)
mk_isl (value; sumSyntax)
mk_isprefix (value; stringSyntax)
mk_isr (value; sumSyntax)
mk_istream (value; Lib)
mk_K (value; combinSyntax)
mk_K_1 (value; combinSyntax)
mk_lam (value; Absyn)
mk_last (value; listSyntax)
mk_least (value; numSyntax)
mk_length (value; listLib, listSyntax)
mk_leq (value; intSyntax, numSyntax)
mk_less (value; intSyntax, numSyntax)
mk_let (value; Psyntax, Rsyntax, boolSyntax)
mk_lex (value; pairSyntax)
mk_linv (value; pred_setSyntax)
mk_list (value; listLib, listSyntax)
mk_list_case (value; listSyntax)
mk_list_type (value; listLib, listSyntax)
mk_literal_case (value; boolSyntax)
mk_local_grms (value; Parse)
mk_map (value; listLib, listSyntax)
mk_map2 (value; listLib, listSyntax)
mk_max (value; numSyntax)
mk_max_set (value; pred_setSyntax)
mk_measure (value; numSyntax)
mk_mem (value; listLib, listSyntax)
mk_meter (value; Count)
mk_min (value; numSyntax)
mk_min_set (value; pred_setSyntax)
mk_minus (value; intSyntax, numSyntax)
mk_mod (value; intSyntax, numSyntax)
mk_mult (value; intSyntax, numSyntax)
mk_n2w (value; wordsSyntax)
mk_neg (value; boolSyntax)
mk_negated (value; intSyntax)
mk_nil (value; listLib, listSyntax)
mk_nondatatype_info (value; TypeBasePure)
mk_none (value; optionLib, optionSyntax)
mk_null (value; listLib, listSyntax)
mk_num_case (value; numSyntax)
mk_numeral (value; numSyntax)
mk_nzcv (value; wordsSyntax)
mk_o (value; combinSyntax)
mk_odd (value; numSyntax)
mk_option (value; optionLib, optionSyntax)
mk_option_case (value; optionLib, optionSyntax)
mk_option_join (value; optionLib, optionSyntax)
mk_option_map (value; optionLib, optionSyntax)
mk_oracle_thm (value; Thm)
mk_ord (value; stringLib, stringSyntax)
mk_outl (value; sumSyntax)
mk_outr (value; sumSyntax)
MK_PABS (value; PairRules)
mk_pabs (value; pairLib, pairSyntax)
MK_PAIR (value; PairRules)
mk_pair (value; Absyn, pairLib, pairSyntax)
mk_pair_map (value; pairLib, pairSyntax)
MK_PEXISTS (value; PairRules)
mk_pexists (value; pairLib, pairSyntax)
mk_pexists1 (value; pairLib, pairSyntax)
MK_PFORALL (value; PairRules)
mk_pforall (value; pairLib, pairSyntax)
mk_plet (value; pairSyntax)
mk_plus (value; intSyntax, numSyntax)
mk_pow (value; pred_setSyntax)
mk_pre (value; numSyntax)
mk_primed_var (value; Psyntax, Rsyntax, Term)
mk_prod (value; pairLib, pairSyntax)
MK_PSELECT (value; PairRules)
mk_pselect (value; pairLib, pairSyntax)
mk_psubset (value; pred_setSyntax)
mk_rat_add (value; ratSyntax)
mk_rat_ainv (value; ratSyntax)
mk_rat_div (value; ratSyntax)
mk_rat_dnm (value; ratSyntax)
mk_rat_minv (value; ratSyntax)
mk_rat_mul (value; ratSyntax)
mk_rat_nmr (value; ratSyntax)
mk_rat_sgn (value; ratSyntax)
mk_rat_sub (value; ratSyntax)
mk_Rdefn (value; Defn)
mk_record (value; TypeBase, TypeBasePure)
mk_res_abstract (value; boolSyntax)
mk_res_exists (value; boolSyntax)
mk_res_exists_unique (value; boolSyntax)
mk_res_forall (value; boolSyntax)
mk_res_select (value; boolSyntax)
mk_rest (value; pred_setSyntax)
mk_reverse (value; listSyntax)
mk_rewrites (value; Ho_Rewrite, Rewrite)
mk_ring_thm (value; ringLib)
mk_rinv (value; pred_setSyntax)
mk_S (value; combinSyntax)
mk_select (value; Absyn, Psyntax, Rsyntax, boolSyntax)
mk_set (value; Lib, pred_setSyntax)
mk_set_spec (value; pred_setSyntax)
mk_set_type (value; pred_setSyntax)
mk_simpset (value; simpLib)
mk_sing (value; pred_setSyntax)
mk_snd (value; pairLib, pairSyntax)
mk_some (value; optionLib, optionSyntax)
mk_state (value; holCheckLib)
mk_strcat (value; stringSyntax)
mk_string (value; stringLib, stringSyntax)
mk_string_case (value; stringSyntax)
mk_strlen (value; stringSyntax)
mk_sub_bag (value; bagLib, bagSyntax)
mk_subset (value; pred_setSyntax)
mk_suc (value; numSyntax)
mk_sum (value; listLib, listSyntax, sumSyntax)
mk_sum_case (value; sumSyntax)
mk_sum_image (value; pred_setSyntax)
mk_sum_set (value; pred_setSyntax)
mk_surj (value; pred_setSyntax)
mk_sw2sw (value; wordsSyntax)
mk_the (value; optionLib, optionSyntax)
mk_thm (value; Thm)
mk_thy_const (value; Term)
mk_thy_type (value; Type)
mk_time (value; Portable)
mk_tl (value; listLib, listSyntax)
mk_type (value; Psyntax, Rsyntax, Type)
mk_typed (value; Absyn)
mk_uncurry (value; pairLib, pairSyntax)
mk_union (value; bagLib, bagSyntax, pred_setSyntax)
mk_univ (value; pred_setSyntax)
mk_unzip (value; listLib, listSyntax)
mk_var (value; Psyntax, Rsyntax, Term)
mk_vartype (value; Type)
mk_W (value; combinSyntax)
mk_w2n (value; wordsSyntax)
mk_w2w (value; wordsSyntax)
mk_while (value; numSyntax)
mk_word_1comp (value; wordsSyntax)
mk_word_2comp (value; wordsSyntax)
mk_word_add (value; wordsSyntax)
mk_word_and (value; wordsSyntax)
mk_word_asr (value; wordsSyntax)
mk_word_bit (value; wordsSyntax)
mk_word_bits (value; wordsSyntax)
mk_word_concat (value; wordsSyntax)
mk_word_extract (value; wordsSyntax)
mk_word_ge (value; wordsSyntax)
mk_word_gt (value; wordsSyntax)
mk_word_H (value; wordsSyntax)
mk_word_hi (value; wordsSyntax)
mk_word_hs (value; wordsSyntax)
mk_word_join (value; wordsSyntax)
mk_word_L (value; wordsSyntax)
mk_word_le (value; wordsSyntax)
mk_word_lo (value; wordsSyntax)
mk_word_log2 (value; wordsSyntax)
mk_word_ls (value; wordsSyntax)
mk_word_lsb (value; wordsSyntax)
mk_word_lsl (value; wordsSyntax)
mk_word_lsr (value; wordsSyntax)
mk_word_lt (value; wordsSyntax)
mk_word_modify (value; wordsSyntax)
mk_word_msb (value; wordsSyntax)
mk_word_mul (value; wordsSyntax)
mk_word_or (value; wordsSyntax)
mk_word_reverse (value; wordsSyntax)
mk_word_rol (value; wordsSyntax)
mk_word_ror (value; wordsSyntax)
mk_word_rrx (value; wordsSyntax)
mk_word_size (value; wordsLib)
mk_word_slice (value; wordsSyntax)
mk_word_sub (value; wordsSyntax)
mk_word_T (value; wordsSyntax)
mk_word_type (value; wordsSyntax)
mk_word_xor (value; wordsSyntax)
mk_xable (value; Systeml)
mk_zip (value; listLib, listSyntax)
MkComb (constructor; Count)
MkIterThms (value; DerivedBddRules)
MkPrevThm (value; DerivedBddRules)
mlquote (value; Lib)
Mod (exception; Portable)
mod (value; Arbint, Arbnum)
mod2 (value; Arbnum)
mod_2exp_tm (value; numSyntax)
MOD_CONV (value; reduceLib)
mod_tm (value; intSyntax, numSyntax)
model (type; holCheckLib)
monitoring (value; Defn, Rewrite, computeLib)
MONO_TAC (value; InductiveDefinition)
monoset (type; IndDefLib, InductiveDefinition)
MOSMLDIR (value; Systeml)
Mp (constructor; Count)
MP (value; Thm)
MP_TAC (value; Tactic)
MUL_CANON_CONV (value; numSimps)
MUL_CONV (value; reduceLib)
mult_tm (value; intSyntax, numSyntax)
MUTREC (constructor; DefnBase)

N

n2w_tm (value; wordsSyntax)
name (value; PrimitiveBddRules)
name_of (value; Defn)
name_of_const (value; liteLib)
nameError (exception; PrimitiveBddRules)
nameStrm (value; Lexis)
nchotomy_of (value; TypeBase, TypeBasePure)
ndefs (value; defCNF)
NEG_DISCH (value; Drule)
negate (value; Arbint)
negate_tm (value; intSyntax)
negation (value; boolSyntax)
NEQ_CONV (value; reduceLib)
NESTREC (constructor; DefnBase)
Net (structure)
net (type; Ho_Net, Net)
net_of (value; Rewrite)
new_axiom (value; Theory, hol88Lib)
new_binder (value; Psyntax, Rsyntax, boolSyntax)
new_binder_definition (value; boolSyntax)
new_compset (value; computeLib)
new_constant (value; Psyntax, Rsyntax, Theory, boolSyntax)
new_datatype (value; Datatype)
new_definition (value; Definition, Q)
new_definition_hook (value; Definition)
new_inductive_definition (value; InductiveDefinition)
new_infix (value; Psyntax, Rsyntax, boolSyntax)
new_infix_prim_rec_definition (value; hol88Lib)
new_infix_type (value; boolSyntax)
new_infixl_definition (value; Q, boolSyntax)
new_infixr_definition (value; Q, boolSyntax)
new_let_thms (value; BasicProvers)
new_prim_rec_definition (value; hol88Lib)
new_recursive_definition (value; Prim_rec)
new_specification (value; Definition, Rsyntax)
new_specification_hook (value; Definition)
new_theory (value; Theory)
new_type (value; Psyntax, Rsyntax, Theory, boolSyntax)
new_type_definition (value; Definition, boolSyntax)
next (value; Lib)
nil_tm (value; listLib, listSyntax)
NNF_CONV (value; Canon)
NNF_SKOLEM_CONV (value; Canon)
NNFC_CONV (value; Canon_Port)
NO_CONV (value; Conv)
NO_TAC (value; Tactical)
NO_THEN (value; Thm_cont)
non_presburger_subterms (value; Cooper)
NONASSOC (value; Parse)
none_tm (value; optionLib, optionSyntax)
NONREC (constructor; DefnBase)
NoPhrasing (value; Parse)
norm_quote (value; Portable)
norm_subst (value; Term)
NORM_TAC (value; BasicProvers)
NOT_CONV (value; reduceLib)
NOT_ELIM (value; Thm)
NOT_EQ_SYM (value; Drule)
NOT_EXISTS_CONV (value; Conv)
NOT_FORALL_CONV (value; Conv)
NOT_INTRO (value; Thm)
NOT_PEXISTS_CONV (value; PairRules)
NOT_PFORALL_CONV (value; PairRules)
NOT_ss (value; boolSimps)
NotElim (constructor; Count)
notify_on_tyvar_guess (value; Globals)
NotIntro (constructor; Count)
NTAC (value; Tactic)
Ntimes (value; Drule)
null_intersection (value; Lib)
null_tm (value; listLib, listSyntax)
num (type; Arbint, Arbnum, Theory)
num (value; numSyntax)
num_case_tm (value; numSyntax)
num_compset (value; reduceLib)
num_CONV (value; numLib)
NUM_NORM_CONV (value; numRingLib)
NUM_NORM_RULE (value; numRingLib)
NUM_NORM_TAC (value; numRingLib)
NUM_RING_CONV (value; numRingLib)
NUM_RING_RULE (value; numRingLib)
NUM_RING_TAC (value; numRingLib)
num_ss (value; numLib)
numbers (value; Lexis)
numeral_tm (value; numSyntax)
numLib (structure)
numRingLib (structure)
numSimps (structure)
numSyntax (structure)
nzcv_tm (value; wordsSyntax)

O

o_tm (value; combinSyntax)
ODD_CONV (value; reduceLib)
odd_tm (value; numSyntax)
ok_identifier (value; Lexis)
ok_sml_identifier (value; Lexis)
ok_symbolic (value; Lexis)
old (value; Globals)
old_ARITH_ss (value; bossLib, numSimps)
old_arith_ss (value; bossLib)
on (value; SingleStep)
Once (value; Drule)
ONCE_ASM_REWRITE_RULE (value; Ho_Rewrite, Rewrite)
ONCE_ASM_REWRITE_TAC (value; Ho_Rewrite, Rewrite)
ONCE_DEPTH_CONV (value; Conv, liteLib)
ONCE_DEPTH_QCONV (value; liteLib)
ONCE_REWRITE_CONV (value; Ho_Rewrite, Rewrite)
ONCE_REWRITE_RULE (value; Ho_Rewrite, Rewrite)
ONCE_REWRITE_TAC (value; Ho_Rewrite, Rewrite)
one (value; Arbint, Arbnum)
one_one_of (value; TypeBase, TypeBasePure)
one_tm (value; intSyntax)
ONEWAY_SKOLEM_CONV (value; Canon)
OnlyIfNecessary (value; Parse)
oo (value; hol88Lib)
op_arity (value; Type)
op_insert (value; Lib)
op_intersect (value; Lib)
op_mem (value; Lib)
op_mk_set (value; Lib)
op_set_diff (value; Lib)
op_U (value; Lib)
op_union (value; Lib)
open_in (value; Portable)
open_out (value; Portable)
option_app (value; liteLib)
option_case_tm (value; optionLib, optionSyntax)
option_cases (value; liteLib)
option_join_tm (value; optionLib, optionSyntax)
option_map_tm (value; optionLib, optionSyntax)
OPTION_rws (value; optionLib)
option_rws (value; optionLib)
OPTION_ss (value; optionSimps)
optionLib (structure)
optionSimps (structure)
optionSyntax (structure)
OR_CONV (value; reduceLib)
OR_EXISTS_CONV (value; Conv)
OR_FORALL_CONV (value; Conv)
OR_PEXISTS_CONV (value; PairRules)
OR_PFORALL_CONV (value; PairRules)
Oracle (constructor; Count)
ORD_CHR_CONV (value; stringLib)
ord_of_lt (value; liteLib)
ord_tm (value; stringLib, stringSyntax)
ordof (value; Portable)
ORELSE (value; Tactical, jrhTactics)
ORELSE_TCL (value; Thm_cont, jrhTactics)
ORELSEC (value; Conv)
orelsef (value; liteLib)
ORIG (constructor; TypeBasePure)
OS (value; Systeml)
outl_tm (value; sumSyntax)
output (value; Portable)
outputc (value; Portable)
outr_tm (value; sumSyntax)
outstream (type; Portable)
overinfo (type; Preterm)
overload_on (value; Parse)
overload_on_by_nametype (value; Parse)
Overloaded (constructor; Preterm)
overloading_resolution (value; Preterm)

P

p (value; goalstackLib)
P_FUN_EQ_CONV (value; PairRules)
P_PCHOOSE_TAC (value; PairRules)
P_PCHOOSE_THEN (value; PairRules)
P_PGEN_TAC (value; PairRules)
P_PSKOLEM_CONV (value; PairRules)
PABS (value; PairRules)
PABS_CONV (value; PairRules)
paconv (value; PairRules)
pair (value; Lib)
PAIR0_ss (value; pairSimps)
pair2recd (value; hol88Lib)
pair_compare (value; Lib)
PAIR_CONV (value; PairRules)
pair_map_tm (value; pairLib, pairSyntax)
PAIR_ss (value; pairSimps)
PAIRED_BETA_CONV (value; PairedLambda, pairLib)
PAIRED_ETA_CONV (value; PairedLambda, pairLib)
PairedLambda (structure)
pairLib (structure)
PairRules (structure)
pairSimps (structure)
pairSyntax (structure)
pairTools (structure)
PALPHA (value; PairRules)
PALPHA_CONV (value; PairRules)
params_of (value; Defn)
parens (value; Lexis)
ParenStyle (type; Parse)
parents (value; Theory)
ParoundName (value; Parse)
ParoundPrec (value; Parse)
PARSE (constructor; TotalDefn)
Parse (structure)
parse_defn (value; Defn)
parse_from_grammars (value; Parse)
parse_in_context (value; Parse)
parse_preterm_in_context (value; Parse)
PART_MATCH (value; Drule)
PART_PMATCH (value; PairRules)
partial (value; Lib)
partition (value; Lib)
PASS (constructor; Lib)
PAT_ABBREV_TAC (value; Q)
PAT_ASSUM (value; Q, Tactical)
PAT_UNDISCH_TAC (value; Q)
pattern (type; Defn)
PBETA_CONV (value; PairRules)
PBETA_RULE (value; PairRules)
PBETA_TAC (value; PairRules)
pbody (value; pairLib, pairSyntax)
pbvar (value; pairLib, pairSyntax)
PCHOOSE (value; PairRules)
PCHOOSE_TAC (value; PairRules)
PCHOOSE_THEN (value; PairRules)
peek (value; Varmap)
PETA_CONV (value; PairRules)
PEXISTENCE (value; PairRules)
PEXISTS (value; PairRules)
PEXISTS_AND_CONV (value; PairRules)
PEXISTS_CONV (value; PairRules)
PEXISTS_EQ (value; PairRules)
PEXISTS_IMP (value; PairRules)
PEXISTS_IMP_CONV (value; PairRules)
PEXISTS_NOT_CONV (value; PairRules)
PEXISTS_OR_CONV (value; PairRules)
PEXISTS_RULE (value; PairRules)
PEXISTS_TAC (value; PairRules)
PEXISTS_UNIQUE_CONV (value; PairRules)
PEXT (value; PairRules)
PFORALL_AND_CONV (value; PairRules)
PFORALL_EQ (value; PairRules)
PFORALL_IMP_CONV (value; PairRules)
PFORALL_NOT_CONV (value; PairRules)
PFORALL_OR_CONV (value; PairRules)
PFUN_EQ_RULE (value; pairLib, pairTools)
PGEN (value; PairRules, pairLib, pairTools)
PGEN_TAC (value; PairRules, pairLib, pairTools)
PGENL (value; PairRules)
phase (type; TotalDefn)
PhraseBlockStyle (type; Parse)
PINST (value; liteLib)
pluck (value; Lib)
plus1 (value; Arbnum)
plus2 (value; Arbnum)
plus_tm (value; intSyntax, numSyntax)
PMATCH_MP (value; PairRules)
PMATCH_MP_TAC (value; PairRules)
pointer_eq (value; Portable)
polymorphic (value; Type)
POP_ASSUM (value; Tactical, jrhTactics)
POP_ASSUM_LIST (value; Tactical, jrhTactics)
Portable (structure)
pow (value; Arbnum)
pow_tm (value; pred_setSyntax)
pp_defn (value; DefnBase)
pp_element (type; Parse)
pp_flags (value; Globals)
pp_goalstack (value; goalstackLib)
pp_int (value; Arbint)
pp_num (value; Arbnum)
pp_proofs (value; goalstackLib)
pp_rewrites (value; Rewrite)
pp_tag (value; Tag)
pp_term (value; Hol_pp, Parse)
pp_theory (value; Hol_pp)
pp_theory_as_html (value; DB)
pp_thm (value; Hol_pp, Parse, Theory)
pp_to_disk (value; Tag)
pp_tyinfo (value; TypeBasePure)
pp_type (value; Hol_pp, Parse)
pp_with_bquotes (value; Parse)
pp_word (value; wordsLib)
pp_word_bin (value; wordsLib)
pp_word_dec (value; wordsLib)
pp_word_hex (value; wordsLib)
pp_word_oct (value; wordsLib)
PPBlock (value; Parse)
pprint (value; Portable)
ppstream (type; Abbrev, Hol_pp, Parse, Portable, Theory, TypeBasePure)
pr_list (value; Portable)
pr_list_to_ppstream (value; Portable)
PRE_CONV (value; reduceLib)
pre_tm (value; numSyntax)
precheck (value; mesonLib)
pred (type; Ho_Rewrite, Rewrite)
PRED_SET_AC_ss (value; pred_setSimps)
PRED_SET_ss (value; pred_setLib, pred_setSimps)
pred_setLib (structure)
pred_setSimps (structure)
pred_setSyntax (structure)
prefer_form_with_tok (value; Parse)
prefer_int (value; intLib)
prefer_num (value; numLib)
prefine (value; mesonLib)
Prefix (constructor; Parse)
prefix (value; HolSatLib)
PRENEX_CONV (value; Canon, Canon_Port)
PRESIMP_CONV (value; Canon_Port)
Preterm (structure)
preterm (type; Preterm)
Preterm (value; Parse)
pretype (type; Absyn, Preterm)
prim_get (value; TypeBasePure)
prim_mk_const (value; Term)
prim_mk_set (value; pred_setSyntax)
prim_mk_set_spec (value; pred_setSyntax)
Prim_rec (structure)
PRIM_STP_TAC (value; BasicProvers)
PRIM_TC_SIMP_CONV (value; TotalDefn)
PRIM_TC_SIMP_TAC (value; TotalDefn)
prim_variant (value; Term)
PRIM_WF_REL_TAC (value; TotalDefn)
PRIM_WF_TAC (value; TotalDefn)
prim_wfrec_definition (value; Defn)
primDefine (value; TotalDefn)
prime (value; Lib)
primHol_datatype (value; Datatype)
primHol_datatype_from_astl (value; Datatype)
priming (value; Globals)
PrimitiveBddRules (structure)
PRIMREC (constructor; DefnBase)
PRINT_CONV (value; Conv)
print_from_grammars (value; Parse)
print_term (value; Hol_pp, Parse)
print_term_by_grammar (value; Parse)
print_theory (value; DB)
print_theory_as_html (value; DB)
print_theory_to_file (value; DB)
print_theory_to_outstream (value; DB)
print_thm (value; Hol_pp, Parse)
print_thy_loads (value; Globals)
print_type (value; Hol_pp, Parse)
PrintBdd (structure)
prob_canon_ss (value; probLib)
probLib (structure)
proofs (type; Defn, goalstackLib)
PROP_CNF_CONV (value; Canon, Canon_Port)
PROP_DNF_CONV (value; Canon)
protect (value; Systeml)
PROVE (value; BasicProvers, bossLib, hol88Lib)
prove (value; Q, Tactical)
prove_abs_fn_one_one (value; Drule)
prove_abs_fn_onto (value; Drule)
prove_cases_thm (value; Prim_rec)
prove_constructors_distinct (value; Prim_rec)
prove_constructors_one_one (value; Prim_rec)
PROVE_HYP (value; Drule)
prove_induction_thm (value; Prim_rec)
prove_inductive_relations_exist (value; InductiveDefinition)
prove_model (value; holCheckLib)
prove_monotonicity_hyps (value; InductiveDefinition)
prove_nonschematic_inductive_relations_exist (value; InductiveDefinition)
prove_rec_fn_exists (value; Prim_rec)
prove_recordtype_thms (value; RecordType)
prove_rep_fn_one_one (value; Drule)
prove_rep_fn_onto (value; Drule)
PROVE_TAC (value; BasicProvers, bossLib)
prove_tcs (value; Defn)
prove_thm (value; hol88Lib)
proveTotal (value; TotalDefn)
PRUNE_CONV (value; unwindLib)
PRUNE_ONCE_CONV (value; unwindLib)
PRUNE_ONE_CONV (value; unwindLib)
PRUNE_RIGHT_RULE (value; unwindLib)
PRUNE_SOME_CONV (value; unwindLib)
PRUNE_SOME_RIGHT_RULE (value; unwindLib)
PSELECT_CONV (value; PairRules)
PSELECT_ELIM (value; PairRules)
PSELECT_EQ (value; PairRules)
PSELECT_INTRO (value; PairRules)
PSELECT_RULE (value; PairRules)
PSKOLEM_CONV (value; PairRules)
PSPEC (value; PairRules)
PSPEC_ALL (value; PairRules)
PSPEC_PAIR (value; PairRules)
PSPEC_TAC (value; PairRules)
PSPECL (value; PairRules)
PSTRIP_ASSUME_TAC (value; PairRules)
PSTRIP_GOAL_THEN (value; PairRules)
PSTRIP_TAC (value; PairRules)
PSTRIP_THM_THEN (value; PairRules)
PSTRUCT_CASES_TAC (value; PairRules)
PSUB_CONV (value; PairRules)
psubset_tm (value; pred_setSyntax)
Psyntax (structure)
PTAUT_CONV (value; tautLib)
PTAUT_PROVE (value; tautLib)
PTAUT_TAC (value; tautLib)
PURE_ASM_REWRITE_RULE (value; Ho_Rewrite, Rewrite)
PURE_ASM_REWRITE_TAC (value; Ho_Rewrite, Rewrite)
PURE_CASE_TAC (value; SingleStep)
PURE_DEF_CNF_CONV (value; defCNF)
PURE_DEF_CNF_VECTOR_CONV (value; defCNF)
pure_goal (value; Cooper)
PURE_ONCE_ASM_REWRITE_RULE (value; Ho_Rewrite, Rewrite)
PURE_ONCE_ASM_REWRITE_TAC (value; Ho_Rewrite, Rewrite)
PURE_ONCE_REWRITE_CONV (value; Ho_Rewrite, Rewrite)
PURE_ONCE_REWRITE_RULE (value; Ho_Rewrite, Rewrite)
PURE_ONCE_REWRITE_TAC (value; Ho_Rewrite, Rewrite)
PURE_REAL_ARITH_TAC (value; RealArith, realLib)
PURE_REWRITE_CONV (value; Ho_Rewrite, Rewrite)
PURE_REWRITE_RULE (value; Ho_Rewrite, Rewrite)
PURE_REWRITE_TAC (value; Ho_Rewrite, Rewrite)
pure_ss (value; bossLib)
PURE_TOP_CASE_TAC (value; SingleStep)
put_accessors (value; TypeBasePure)
put_encode (value; TypeBasePure)
put_fields (value; TypeBasePure)
put_induction (value; TypeBasePure)
put_lift (value; TypeBasePure)
put_nchotomy (value; TypeBasePure)
put_simpls (value; TypeBasePure)
put_size (value; TypeBasePure)
put_updates (value; TypeBasePure)
pwd (value; Portable)
PWORDLEN_bitop_CONV (value; wordLib)
PWORDLEN_CONV (value; wordLib)
PWORDLEN_TAC (value; wordLib)

Q

Q (structure)
Q_TAC (value; Tactical)
QCHANGED_CONV (value; Conv)
QCONV (value; Conv)
QIDENT (constructor; Absyn)
QUANT_CONV (value; Conv)
quot (value; Arbint)
quot_tm (value; intSyntax)
quotation (type; Abbrev, Absyn, Portable)
quote (value; Lib)
quotrem (value; Arbint)

R

R (value; goalstackLib)
r (value; goalstackLib)
Raise (value; Feedback)
rand (value; Term)
RAND_CONV (value; Conv)
rat_0_tm (value; ratSyntax)
rat_1_tm (value; ratSyntax)
rat_add_tm (value; ratSyntax)
RAT_ADDAC_CONV (value; ratLib)
RAT_ADDAC_TAC (value; ratLib)
RAT_ADDSUB_TAC (value; ratLib)
rat_ainv_tm (value; ratSyntax)
RAT_BASIC_ARITH_CONV (value; ratLib)
RAT_BASIC_ARITH_TAC (value; ratLib)
rat_basic_rewrites (value; ratLib)
RAT_CALC_CONV (value; ratLib)
RAT_CALC_TAC (value; ratLib)
RAT_CALCEQ_TAC (value; ratLib)
RAT_CALCTERM_TAC (value; ratLib)
rat_div_tm (value; ratSyntax)
rat_dnm_tm (value; ratSyntax)
RAT_ELIMINATE_MINV_CONV (value; ratLib)
RAT_ELIMINATE_MINV_EQ_CONV (value; ratLib)
RAT_ELIMINATE_MINV_TAC (value; ratLib)
RAT_EQ_CONV (value; ratLib)
RAT_EQ_LMUL_TAC (value; ratLib)
RAT_EQ_RMUL_TAC (value; ratLib)
RAT_EQ_TAC (value; ratLib)
rat_geq_tm (value; ratSyntax)
rat_gre_tm (value; ratSyntax)
rat_leq_tm (value; ratSyntax)
rat_les_tm (value; ratSyntax)
rat_minv_tm (value; ratSyntax)
rat_mul_tm (value; ratSyntax)
RAT_MULAC_CONV (value; ratLib)
RAT_MULAC_TAC (value; ratLib)
rat_nmr_tm (value; ratSyntax)
rat_num_rewrites (value; ratLib)
RAT_POSTCALC_CONV (value; ratLib)
RAT_PRECALC_CONV (value; ratLib)
rat_rewrites (value; ratLib)
RAT_RING_CONV (value; ratRingLib)
RAT_RING_NORM_CONV (value; ratRingLib)
RAT_RING_NORM_RULE (value; ratRingLib)
RAT_RING_NORM_TAC (value; ratRingLib)
RAT_RING_RULE (value; ratRingLib)
RAT_RING_TAC (value; ratRingLib)
RAT_SAVE_ALLVARS_TAC (value; ratLib)
RAT_SAVE_TAC (value; ratLib)
rat_sgn_tm (value; ratSyntax)
RAT_STRICT_CALC_TAC (value; ratLib)
rat_sub_tm (value; ratSyntax)
ratLib (structure)
rator (value; Term)
RATOR_CONV (value; Conv)
ratRingLib (structure)
RATSKOL (value; Canon)
ratSyntax (structure)
raw_match (value; Term)
raw_match_type (value; Type)
rdistrib_tm (value; boolSyntax)
read (value; Count, Tag, TypeBase)
read_congs (value; DefnBase)
read_disk_tag (value; Tag)
readDimacs (value; HolSatLib)
real_ac_SS (value; realSimps)
real_ac_ss (value; realSimps)
REAL_ARITH (value; RealArith, realLib)
REAL_ARITH_ss (value; realSimps)
REAL_ARITH_TAC (value; RealArith, realLib)
REAL_ASM_ARITH_TAC (value; RealArith)
real_compset (value; realSimps)
REAL_REDUCE_ss (value; realSimps)
real_SS (value; realSimps)
real_ss (value; realLib, realSimps)
RealArith (structure)
realLib (structure)
realSimps (structure)
recd2pair (value; hol88Lib)
recInduct (value; SingleStep, bossLib)
RecordType (structure)
RED_CONV (value; reduceLib)
REDEPTH_CONV (value; Conv, liteLib)
REDEPTH_QCONV (value; liteLib)
REDUCE (value; IndDefRules)
REDUCE_CONV (value; intLib, numLib, reduceLib)
REDUCE_RULE (value; numLib, reduceLib)
REDUCE_ss (value; numSimps)
REDUCE_TAC (value; numLib, reduceLib)
reduceLib (structure)
REFINE_EXISTS_TAC (value; Q)
refinement (type; jrhTactics)
Refl (constructor; Count)
REFL (value; Q, Thm)
REFL_TAC (value; Tactic)
REFUTE (value; Canon)
REFUTE_THEN (value; Canon_Port)
register_btrace (value; Feedback)
register_ftrace (value; Feedback)
register_trace (value; Feedback)
register_update_fn (value; TypeBase)
reify (value; ringLib)
release (value; Globals)
reln_of (value; Defn)
rem (value; Arbint)
rem_tm (value; intSyntax)
remove (value; Varmap)
remove_assoc (value; liteLib)
remove_case_magic (value; Preterm)
remove_numeral_form (value; Parse)
remove_ovl_mapping (value; Parse)
remove_rules_for_term (value; Parse)
remove_termtok (value; Parse)
remove_user_printer (value; Parse)
rename_bvar (value; Term)
RENAME_VARS_CONV (value; Conv)
REPEAT (value; Tactical, jrhTactics)
repeat (value; Lib, liteLib)
REPEAT_GTCL (value; Thm_cont)
REPEAT_TCL (value; Thm_cont)
REPEATC (value; Conv)
REPEATQC (value; liteLib)
replicate (value; hol88Lib, liteLib)
report (value; Count)
res_abstract_tm (value; boolSyntax)
RES_CANON (value; Drule)
res_exists1_tm (value; boolSyntax)
res_exists_tm (value; boolSyntax)
res_forall_tm (value; boolSyntax)
res_quanLib (structure)
res_select_tm (value; boolSyntax)
RES_TAC (value; Tactic)
RES_THEN (value; Thm_cont)
reset (value; Lib)
reset_thm_count (value; Count)
reset_trace (value; Feedback)
reset_traces (value; Feedback)
respect_width_ref (value; Parse)
RESQ_WORDLEN_TAC (value; wordLib)
rest_tm (value; pred_setSyntax)
restart (value; goalstackLib)
restore_prover (value; Tactical)
RESTR_EVAL_CONV (value; computeLib)
RESTR_EVAL_RULE (value; computeLib)
RESTR_EVAL_TAC (value; computeLib)
rev_assoc (value; Lib, hol88Lib, liteLib)
rev_itlist (value; Lib)
rev_itlist2 (value; Lib)
rev_splitlist (value; liteLib)
reveal (value; Parse)
REVERSE (value; Tactical)
reverse_tm (value; listSyntax)
REWR_CONV (value; Conv)
Rewrite (structure)
REWRITE_CONV (value; Ho_Rewrite, Rewrite)
REWRITE_RULE (value; Ho_Rewrite, Rewrite)
REWRITE_TAC (value; Ho_Rewrite, Rewrite)
rewrites (type; Rewrite)
rewrites (value; bossLib, simpLib)
REWRITES_CONV (value; Rewrite)
RF (constructor; Parse)
rhs (value; boolSyntax)
RHS_CONV (value; Conv)
RIGHT (value; Parse)
RIGHT_AND_EXISTS_CONV (value; Conv)
RIGHT_AND_FORALL_CONV (value; Conv)
RIGHT_AND_PEXISTS_CONV (value; PairRules)
RIGHT_AND_PFORALL_CONV (value; PairRules)
RIGHT_BETA (value; Drule)
RIGHT_BETAS (value; liteLib)
RIGHT_CONV_RULE (value; Conv)
RIGHT_IMP_EXISTS_CONV (value; Conv)
RIGHT_IMP_FORALL_CONV (value; Conv)
RIGHT_IMP_PEXISTS_CONV (value; PairRules)
RIGHT_IMP_PFORALL_CONV (value; PairRules)
RIGHT_LIST_BETA (value; Drule)
RIGHT_LIST_PBETA (value; PairRules)
RIGHT_OR_EXISTS_CONV (value; Conv)
RIGHT_OR_FORALL_CONV (value; Conv)
RIGHT_OR_PEXISTS_CONV (value; PairRules)
RIGHT_OR_PFORALL_CONV (value; PairRules)
RIGHT_PBETA (value; PairRules)
RING_CONV (value; ringLib)
RING_NORM_CONV (value; ringLib)
ringLib (structure)
rinv_tm (value; pred_setSyntax)
RM_ABBREV_TAC (value; Q)
RM_ALL_ABBREVS_TAC (value; Q)
rotate (value; goalstackLib, jrhTactics)
rotate_proofs (value; goalstackLib)
rotl (value; liteLib)
rotr (value; liteLib)
Rsyntax (structure)
rule (type; Abbrev, Count)
RULE_ASSUM_TAC (value; Tactic, jrhTactics)
RULE_INDUCT_THEN (value; IndDefRules)
RULE_TAC (value; IndDefRules)
RW_TAC (value; BasicProvers, bossLib)

S

S (value; Lib)
S_tm (value; combinSyntax)
SAME (constructor; Lib)
same_const (value; Term)
Sat_counterexample (exception; HolSatLib)
sat_solver (type; HolSatLib)
SAT_TAUT_PROVE (value; HolSatLib)
satOracle (value; HolSatLib)
satProve (value; HolSatLib)
save (value; hol88Lib)
save_defn (value; Defn)
save_thm (value; Theory)
say (value; Lib)
saying (value; Lib)
sbag_cache (value; bagLib, bagSimps)
SBAG_SOLVE (value; bagLib, bagSimps)
SBAG_SOLVE_ss (value; bagLib, bagSimps)
SBC_CONV (value; reduceLib)
scrub (value; Theory)
scrub_const (value; computeLib)
scrub_thms (value; computeLib)
select (value; boolSyntax)
SELECT_CONV (value; Conv)
SELECT_ELIM (value; Drule)
SELECT_ELIM_TAC (value; Tactic)
SELECT_EQ (value; Drule)
SELECT_INTRO (value; Drule)
SELECT_RULE (value; Drule)
SEQ_CASES_TAC (value; probLib)
set (type; Term, Thm)
set_backup (value; goalstackLib)
set_diff (value; Lib)
set_eq (value; Lib)
set_fixity (value; Parse)
set_flag_abs (value; holCheckLib)
set_flag_ric (value; holCheckLib)
set_goal (value; goalstackLib)
set_goal_pp (value; goalstackLib)
set_implicit_rewrites (value; Ho_Rewrite, Rewrite)
SET_INDUCT_TAC (value; pred_setLib)
set_init (value; holCheckLib)
set_known_constants (value; Parse)
set_MLname (value; Theory)
set_name (value; holCheckLib)
set_props (value; holCheckLib)
set_prover (value; Tactical)
set_reln (value; Defn)
set_skip (value; computeLib)
SET_SPEC_CONV (value; pred_setLib)
SET_SPEC_ss (value; pred_setSimps)
set_state (value; holCheckLib)
set_term_printer (value; Parse)
set_trace (value; Feedback)
set_trans (value; holCheckLib)
set_vord (value; holCheckLib)
setify (value; hol88Lib)
shared_thm (type; TypeBase, TypeBasePure)
SHD_PSEUDO_CONV (value; probLib)
show_assums (value; Globals)
show_axioms (value; Globals)
show_numeral_types (value; Globals)
show_scrub (value; Globals)
show_tags (value; Globals)
show_types (value; Globals)
show_types_verbosely (value; Globals)
showVarmap (value; DerivedBddRules)
SIMP_CONV (value; bossLib, simpLib)
SIMP_PROVE (value; simpLib)
SIMP_RULE (value; bossLib, simpLib)
SIMP_TAC (value; bossLib, simpLib)
simp_tcs (value; Defn)
simpfrag (type; TypeBasePure)
SIMPLE_CHOOSE (value; Drule, liteLib)
SIMPLE_DISJ_CASES (value; liteLib)
SIMPLE_EXISTS (value; Drule)
simpLib (structure)
simpls_of (value; TypeBase, TypeBasePure)
simpset (type; BasicProvers, bossLib, ratLib, simpLib)
sing_tm (value; pred_setSyntax)
SINGLE_DEPTH_CONV (value; liteLib)
SingleStep (structure)
size (value; Net, Varmap)
size_of (value; TypeBase, TypeBasePure)
size_of0 (value; TypeBase, TypeBasePure)
SIZES_ss (value; wordsLib)
SKELIM (value; Canon)
skew (value; mesonLib)
SKOLEM_CONV (value; Canon_Port, Conv)
sml_symbols (value; Lexis)
SMV_AUTOMATON_CONV (value; temporalLib)
smv_call (value; temporalLib)
smv_path (value; temporalLib)
SMV_RUN (value; temporalLib)
SMV_RUN_FILE (value; temporalLib)
smv_tmp_dir (value; temporalLib)
snd (value; Lib)
snd_tm (value; pairLib, pairSyntax)
some_tm (value; optionLib, optionSyntax)
sort (value; Lib)
Spec (constructor; Count)
SPEC (value; Q, Thm)
SPEC_ALL (value; Drule)
SPEC_TAC (value; Q, Tactic)
SPEC_THEN (value; Q)
SPEC_VAR (value; Drule)
Specialize (value; Thm)
SPECL (value; Drule, Q)
SPECL_THEN (value; Q)
spine_pair (value; pairLib, pairSyntax)
spine_prod (value; pairSyntax)
split (value; Lib)
split_after (value; Lib)
split_subst (value; DerivedBddRules)
splitlist (value; liteLib)
SPOSE_NOT_THEN (value; SingleStep, bossLib)
srw_ss (value; BasicProvers, bossLib)
SRW_TAC (value; BasicProvers, bossLib)
SSFRAG (constructor; simpLib)
ssfrag (type; bagLib, bagSimps, bossLib, ratLib, simpLib)
standard_spacing (value; Parse)
start_time (value; Lib)
state (value; Lib)
statecount (value; DerivedBddRules)
status (value; goalstackLib)
std_apiDefine (value; TotalDefn)
std_apiDefineq (value; TotalDefn)
std_binder_precedence (value; Parse)
std_goal_pp (value; goalstackLib)
std_out (value; Portable)
std_ss (value; bossLib)
stdin (value; Portable)
stdOut_ppstream (value; Portable)
STDREC (constructor; DefnBase)
STL_PSEUDO_CONV (value; probLib)
stoppers (value; computeLib)
store_ring (value; ringLib)
store_thm (value; Q, Tactical)
STP_TAC (value; BasicProvers)
strcat_tm (value; stringSyntax)
strictify_thm (value; computeLib)
string_case_tm (value; stringSyntax)
string_EQ_CONV (value; stringLib)
string_of_int (value; hol88Lib)
string_rewrites (value; stringSimps)
STRING_ss (value; stringSimps)
string_tm (value; stringLib, stringSyntax)
string_to_int (value; Lib)
string_ty (value; stringLib, stringSyntax)
stringLib (structure)
stringSimps (structure)
stringSyntax (structure)
strip_abs (value; Term, boolSyntax)
strip_anylet (value; pairSyntax)
strip_app (value; Absyn)
STRIP_ASSUME_TAC (value; Tactic)
strip_biginter (value; pred_setSyntax)
strip_bigunion (value; pred_setSyntax)
strip_binder (value; Term)
STRIP_BINDER_CONV (value; Conv)
strip_binop (value; liteLib)
strip_case (value; TypeBase, TypeBasePure)
strip_comb (value; boolSyntax)
strip_conj (value; Absyn, boolSyntax)
strip_disj (value; Absyn, boolSyntax)
strip_exists (value; Absyn, boolSyntax)
strip_exists1 (value; Absyn)
strip_forall (value; Absyn, boolSyntax)
strip_fun (value; boolSyntax)
STRIP_GOAL_THEN (value; Tactic)
strip_imp (value; Absyn, boolSyntax, liteLib)
strip_imp_only (value; boolSyntax)
strip_lam (value; Absyn)
strip_mult (value; intSyntax, numSyntax)
strip_neg (value; boolSyntax)
strip_pabs (value; pairLib, pairSyntax)
strip_pair (value; Absyn, pairLib, pairSyntax)
strip_pexists (value; pairLib, pairSyntax)
strip_pforall (value; pairLib, pairSyntax)
strip_plus (value; intSyntax, numSyntax)
strip_prod (value; pairLib, pairSyntax)
STRIP_QUANT_CONV (value; Conv)
strip_rat_add (value; ratSyntax)
strip_rat_mul (value; ratSyntax)
strip_res_exists (value; boolSyntax)
strip_res_forall (value; boolSyntax)
strip_select (value; Absyn)
strip_set (value; pred_setSyntax)
strip_sum (value; sumSyntax)
STRIP_TAC (value; Tactic)
STRIP_THM_THEN (value; Thm_cont)
strip_union (value; bagLib, bagSyntax)
striplist (value; liteLib)
strlen_tm (value; stringSyntax)
STRUCT_CASES_TAC (value; Tactic)
STRUCT_ERR (value; liteLib)
STRUCT_WRAP (value; liteLib)
SUB_BAG_tm (value; bagLib, bagSyntax)
SUB_CONV (value; Conv, liteLib)
SUB_QCONV (value; liteLib)
SUBGOAL_THEN (value; Q, Tactical)
SUBS (value; Drule)
SUBS_OCCS (value; Drule)
subset_tm (value; pred_setSyntax)
Subst (constructor; Count)
subst (type; Abbrev, Lib, Term)
SUBST (value; Thm, hol88Lib)
subst (value; Term, hol88Lib)
SUBST1_TAC (value; Tactic)
SUBST_ALL_TAC (value; Tactic)
subst_assoc (value; Lib)
SUBST_CONV (value; Drule, hol88Lib)
SUBST_MATCH (value; Ho_Rewrite, Rewrite)
subst_occs (value; hol88Lib)
SUBST_OCCS_TAC (value; Tactic)
subst_of (value; hol88Lib)
SUBST_TAC (value; Tactic)
subtract (value; Lib)
SUC_CONV (value; reduceLib)
SUC_ELIM_CONV (value; numLib)
SUC_FILTER_ss (value; numSimps)
suc_tm (value; numSyntax)
SUC_TO_NUMERAL_DEFN_CONV (value; TotalDefn, numLib)
SUC_TO_NUMERAL_DEFN_CONV_hook (value; Defn)
SUFF_TAC (value; Tactic)
Suffix (value; Parse)
sum (type; sumSyntax)
sum_case_tm (value; sumSyntax)
sum_image_tm (value; pred_setSyntax)
SUM_rws (value; sumSimps)
sum_set_tm (value; pred_setSyntax)
SUM_ss (value; sumSimps)
sum_tm (value; listLib, listSyntax)
sumSimps (structure)
sumSyntax (structure)
surj_tm (value; pred_setSyntax)
sw2sw_tm (value; wordsSyntax)
SWAP_EXISTS_CONV (value; Conv)
SWAP_PEXISTS_CONV (value; PairRules)
SWAP_PFORALL_CONV (value; PairRules)
SWAP_VARS_CONV (value; Conv)
Sym (constructor; Count)
SYM (value; Thm)
SYM_CONV (value; Conv)
system (value; Portable)
system_ps (value; Systeml)
Systeml (structure)
systeml (value; Systeml)

T

T (value; boolSyntax)
TAC_PROOF (value; Tactical)
Tactic (structure)
Tactic (type; jrhTactics)
tactic (type; Abbrev, RealArith, mesonLib, ratLib, realLib)
Tactical (structure)
Tag (structure)
tag (type; Tag, Thm)
tag (value; Thm)
TAUT (value; tautLib)
TAUT_CONV (value; tautLib)
TAUT_PROVE (value; tautLib)
TAUT_TAC (value; tautLib)
tautLib (structure)
TC_SIMP_CONV (value; TotalDefn)
TC_SIMP_TAC (value; TotalDefn)
tcs_of (value; Defn)
temp_add_bare_numeral_form (value; Parse)
temp_add_binder (value; Parse)
temp_add_infix (value; Parse)
temp_add_infix_type (value; Parse)
temp_add_listform (value; Parse)
temp_add_numeral_form (value; Parse)
temp_add_record_field (value; Parse)
temp_add_record_fupdate (value; Parse)
temp_add_rule (value; Parse)
temp_add_type (value; Parse)
temp_add_user_printer (value; Parse)
temp_associate_restriction (value; Parse)
temp_clear_overloads_on (value; Parse)
temp_clear_prefs_for_term (value; Parse)
TEMP_DEFS_CONV (value; temporalLib)
temp_disable_tyabbrev_printing (value; Parse)
temp_give_num_priority (value; Parse)
TEMP_NORMALIZE_CONV (value; temporalLib)
temp_overload_on (value; Parse)
temp_overload_on_by_nametype (value; Parse)
temp_prefer_form_with_tok (value; Parse)
temp_remove_numeral_form (value; Parse)
temp_remove_ovl_mapping (value; Parse)
temp_remove_rules_for_term (value; Parse)
temp_remove_termtok (value; Parse)
temp_remove_user_printer (value; Parse)
temp_set_associativity (value; Parse)
temp_set_fixity (value; Parse)
temp_set_grammars (value; Parse)
temp_type_abbrev (value; Parse)
temporalLib (structure)
Term (structure)
term (type; Abbrev, Absyn, Canon, DB, Definition, DefnBase, DerivedBddRules, Ho_Net, Hol_pp, Net, Parse, Preterm, Psyntax, RealArith, Rsyntax, Term, Theory, Thm, TypeBase, TypeBasePure, boolSyntax, probLib, ratLib, ratSyntax, realLib, temporalLib, unwindLib)
Term (value; Parse)
term_bdd (type; DerivedBddRules, PrimitiveBddRules, holCheckLib)
term_eq (value; Term)
term_grammar (value; Parse)
term_of (value; IndDefLib)
term_of_absyn (value; IndDefLib)
term_of_int (value; intSyntax, numSyntax)
term_pp_prefix (value; Globals)
term_pp_suffix (value; Globals)
term_pp_with_delimiters (value; Parse)
term_to_string (value; Hol_pp, Parse)
termApply (value; PrimitiveBddRules)
TermBddToEqThm (value; DerivedBddRules)
TERMINATION (constructor; TotalDefn)
termToDimacsFile (value; HolSatLib)
termToTermBdd (value; DerivedBddRules)
termToTermBddError (exception; DerivedBddRules)
termToTermBddFun (value; DerivedBddRules)
tgoal (value; Defn)
the (value; liteLib)
the_compset (value; computeLib)
the_monoset (value; IndDefLib)
the_tm (value; optionLib, optionSyntax)
the_value (value; boolSyntax)
THEN (value; Tactical, jrhTactics)
THEN1 (value; Tactical)
THEN_TCL (value; Thm_cont)
THENC (value; Conv)
THENCQC (value; liteLib)
thenf (value; liteLib)
THENL (value; Tactical, jrhTactics)
THENQC (value; liteLib)
theorem (value; DB)
theorems (value; DB)
THEORY (constructor; Hol_pp)
Theory (structure)
theory (type; DB, Hol_pp)
theTypeBase (value; TypeBase)
Thm (constructor; DB)
Thm (structure)
thm (type; Abbrev, Canon, DB, Definition, DefnBase, DerivedBddRules, Hol_pp, Parse, RealArith, Rsyntax, Theory, Thm, TypeBase, TypeBasePure, boolSyntax, mesonLib, probLib, ratLib, realLib, temporalLib, unwindLib)
Thm_cont (structure)
thm_count (value; Count)
thm_frees (value; Thm)
Thm_Tactic (type; jrhTactics)
thm_tactic (type; Abbrev)
Thm_Tactical (type; jrhTactics)
thm_tactical (type; Abbrev)
thm_to_string (value; Hol_pp, Parse)
thms (value; DB)
thmToTermBdd (value; DerivedBddRules)
thry (type; Defn)
thy (value; DB)
thy_addon (type; Theory)
time (type; Portable)
time (value; Lib)
time_eq (value; Portable)
time_lt (value; Portable)
time_to_string (value; Portable)
times2 (value; Arbnum)
timestamp (value; Portable)
tl_tm (value; listLib, listSyntax)
TM (value; Parse)
tmp_name (value; HolSatLib)
tmquote (type; Q)
tmvar_vary (value; Lexis)
to_term (value; Preterm)
toBinString (value; Arbnum)
toHexString (value; Arbnum)
toInt (value; Arbint, Arbnum)
TOK (value; Parse)
toNat (value; Arbint)
toOctString (value; Arbnum)
TOP_DEPTH_CONV (value; Conv, liteLib)
TOP_DEPTH_QCONV (value; liteLib)
top_goal (value; goalstackLib)
top_goals (value; goalstackLib)
TOP_SWEEP_CONV (value; Conv, liteLib)
TOP_SWEEP_QCONV (value; liteLib)
top_thm (value; goalstackLib)
toReal (value; Arbnum)
toString (value; Arbint, Arbnum)
total (value; Lib)
TotalDefn (structure)
tprove (value; Defn)
trace (value; Feedback)
traceBack (value; DerivedBddRules)
traceBackPrevThm (value; DerivedBddRules)
traces (value; Feedback)
Trans (constructor; Count)
TRANS (value; Thm)
traversedata_for_ss (value; simpLib)
TruePrefix (value; Parse)
TRY (value; Tactical)
try (value; Lib)
TRY_CONV (value; Conv)
trye (value; Lib)
tryfind (value; Lib)
tstore_defn (value; Defn)
TUPLE (value; pairLib, pairTools)
TUPLE_TAC (value; pairLib, pairTools)
two (value; Arbint, Arbnum)
ty_antiq (value; Parse)
ty_name_of (value; TypeBasePure)
ty_of (value; TypeBasePure)
tyinfo (type; Datatype, TypeBase, TypeBasePure)
Type (structure)
Type (value; Parse)
type_abbrev (value; Parse)
type_constructors (value; Prim_rec)
type_constructors_with_args (value; Prim_rec)
type_encode (value; TypeBasePure)
type_grammar (value; Parse)
type_lift (value; TypeBasePure)
type_of (value; Term)
type_pp_prefix (value; Globals)
type_pp_suffix (value; Globals)
type_pp_with_delimiters (value; Parse)
type_rws (value; bossLib)
type_size (value; TypeBasePure)
type_ssfrag (value; simpLib)
type_subst (value; Type, hol88Lib)
type_to_string (value; Hol_pp, Parse)
type_var_in (value; Type)
type_vars (value; Type)
type_vars_in_term (value; Term)
type_varsl (value; Type)
TypeBase (structure)
typeBase (type; Datatype, TypeBase, TypeBasePure)
TypeBasePure (structure)
typecheck (value; Preterm)
typecheck_phase1 (value; Preterm)
TYPED (constructor; Absyn)
typedTerm (value; Parse)
types (value; Theory)
typeValue (value; TypeBasePure)
tyquote (type; Q)
tyspec (type; Datatype, ind_types)
tyValue (value; TypeBasePure)
tyvar_ids (value; Lexis)
tyvar_vary (value; Lexis)
tyvars (value; hol88Lib)
tyvarsl (value; hol88Lib)

U

U (value; Lib)
UNABBREV_ALL_TAC (value; Q)
UNABBREV_TAC (value; Q)
UNBETA_CONV (value; Conv)
UNCHANGED (exception; Conv)
uncurry (value; Lib)
UNCURRY_CONV (value; PairRules)
UNCURRY_EXISTS_CONV (value; PairRules)
UNCURRY_FORALL_CONV (value; PairRules)
uncurry_tm (value; pairLib, pairSyntax)
UNDISCH (value; Drule)
UNDISCH_ALL (value; Drule)
UNDISCH_TAC (value; Q, Tactic)
UNDISCH_THEN (value; Q, Thm_cont)
UNFOLD_CONV (value; unwindLib)
UNFOLD_RIGHT_RULE (value; unwindLib)
UNIFORM_CONV (value; probLib)
unify (value; Varmap)
unifyVarmapError (exception; Varmap)
union (value; Lib, Net)
UNION_CONV (value; pred_setLib)
union_defn (value; Defn)
union_tm (value; pred_setSyntax)
univ_tm (value; pred_setSyntax)
universal (value; boolSyntax)
UNLAMB_CONV (value; Canon)
UNPBETA_CONV (value; PairRules)
unprime (value; Lib)
UNSAFE_LTL2OMEGA_CONV (value; temporalLib)
UNSAFE_LTL_CONV (value; temporalLib)
UNSAFE_TEMP_DEFS_CONV (value; temporalLib)
unstrip_pair (value; pairLib, pairSyntax)
UNWIND_ALL_BUT_CONV (value; unwindLib)
UNWIND_ALL_BUT_RIGHT_RULE (value; unwindLib)
UNWIND_AUTO_CONV (value; unwindLib)
UNWIND_AUTO_RIGHT_RULE (value; unwindLib)
UNWIND_CONV (value; unwindLib)
UNWIND_ONCE_CONV (value; unwindLib)
UNWIND_ss (value; boolSimps)
unwindLib (structure)
unzip (value; Lib)
unzip_tm (value; listLib, listSyntax)
update_grms (value; Parse)
update_overload_maps (value; Parse)
update_tyinfo (value; RecordType)
updates_of (value; TypeBase, TypeBasePure)
upto (value; Lib, liteLib)
uptodate_term (value; Theory)
uptodate_thm (value; Theory)
uptodate_type (value; Theory)

V

VALID (value; Tactical)
validation (type; Abbrev)
VAQ (constructor; Absyn)
VAR (constructor; Psyntax, Rsyntax)
Var (constructor; Preterm)
var_compare (value; Term)
VAR_EQ_TAC (value; BasicProvers)
var_occurs (value; Term)
variant (value; Term, hol88Lib)
Varmap (structure)
varmap (type; DerivedBddRules, PrimitiveBddRules, Varmap)
verdict (type; Lib)
verdict (value; Lib)
version (value; Globals)
via (value; Tactic)
VIDENT (constructor; Absyn)
VPAIR (constructor; Absyn)
vstruct (type; Absyn)
VTYPED (constructor; Absyn)

W

W (value; Lib)
w2n_tm (value; wordsSyntax)
w2w_tm (value; wordsSyntax)
W_tm (value; combinSyntax)
WARNING_outstream (value; Feedback)
WARNING_to_string (value; Feedback)
WEAK_CBV_CONV (value; computeLib)
WEAKEN_TAC (value; Tactic)
WF_REL_TAC (value; TotalDefn, bossLib)
WF_TAC (value; TotalDefn)
wfrec_eqns (value; Defn)
while_tm (value; numSyntax)
with_exn (value; Lib)
with_flag (value; Lib)
with_ppstream (value; Portable)
word_1comp_tm (value; wordsSyntax)
word_2comp_tm (value; wordsSyntax)
word_add_tm (value; wordsSyntax)
word_and_tm (value; wordsSyntax)
word_asr_tm (value; wordsSyntax)
word_bit_tm (value; wordsSyntax)
word_bits_tm (value; wordsSyntax)
word_CASES_TAC (value; wordLib)
word_concat_tm (value; wordsSyntax)
word_extract_tm (value; wordsSyntax)
word_ge_tm (value; wordsSyntax)
word_gt_tm (value; wordsSyntax)
word_H_tm (value; wordsSyntax)
word_hi_tm (value; wordsSyntax)
word_hs_tm (value; wordsSyntax)
word_INDUCT_TAC (value; wordLib)
word_join_tm (value; wordsSyntax)
word_L_tm (value; wordsSyntax)
word_le_tm (value; wordsSyntax)
word_lo_tm (value; wordsSyntax)
word_log2_tm (value; wordsSyntax)
word_ls_tm (value; wordsSyntax)
word_lsb_tm (value; wordsSyntax)
word_lsl_tm (value; wordsSyntax)
word_lsr_tm (value; wordsSyntax)
word_lt_tm (value; wordsSyntax)
word_modify_tm (value; wordsSyntax)
word_msb_tm (value; wordsSyntax)
word_mul_tm (value; wordsSyntax)
word_or_tm (value; wordsSyntax)
word_reverse_tm (value; wordsSyntax)
word_rol_tm (value; wordsSyntax)
word_ror_tm (value; wordsSyntax)
word_rrx_tm (value; wordsSyntax)
word_slice_tm (value; wordsSyntax)
word_sub_tm (value; wordsSyntax)
word_T_tm (value; wordsSyntax)
word_xor_tm (value; wordsSyntax)
wordLib (structure)
words2 (value; Lib)
words_compset (value; wordsLib)
WORDS_CONV (value; wordsLib)
WORDS_RULE (value; wordsLib)
WORDS_TAC (value; wordsLib)
wordsLib (structure)
wordsSyntax (structure)
wrap_exn (value; Feedback)
wrap_exn_loc (value; Feedback)
write (value; TypeBase)
write_congs (value; DefnBase)
write_datatype_info (value; computeLib)
write_tyinfos (value; Datatype)
WSEG_CONV (value; wordLib)
WSEG_WSEG_CONV (value; wordLib)

X

X_CASES_THEN (value; Thm_cont)
X_CASES_THENL (value; Thm_cont)
X_CHOOSE_TAC (value; Q, Tactic)
X_CHOOSE_THEN (value; Q, Thm_cont)
X_FUN_EQ_CONV (value; Conv, Q)
X_GEN_TAC (value; Q, Tactic)
X_SKOLEM_CONV (value; Conv, Q)
xable_string (value; Systeml)
xDefine (value; TotalDefn, bossLib)
xDefineSchema (value; TotalDefn)

Z

ZAP_TAC (value; bossLib)
zchaff (value; HolSatLib)
zero (value; Arbint, Arbnum)
zero_tm (value; intSyntax, numSyntax)
zip (value; Lib)
zip_tm (value; listLib, listSyntax)

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

HOL 4, Kananaskis-3