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