HOL Reference Page

LIBRARIES

ai     alist_tree     alist     ASCIInumbers     Backchaining     bag     bagSimple     binary_ieee     bitArith     bit     bitstring     blast     boss     CoIndDef     combin     compute     cong     constrFamilies     countable_types     cv_compute     cv_mem     cv_misc     cv_rep     cv_trans     cv_type     EVAL_numRing     EVAL_ring     fcp     finite_map     flookup     frac     hhExport     hol88     HolSat     HolSmt     IndDef     integer_word     integerRing     intExtension     int     isqrt     list     lite     machine_ieee     marker     meson     metis     native_ieee     num     numposrep     option     pair     patricia_casts     patricia     patternMatches     perm     pred_set     proofManager     quantHeuristics     rat     ratRing     real     reduce     refute     res_quan     simp     sorting     sptree     state_monad     string     tailrec     taut     temporal     transfer     unwind     update     wlog     words    

THEORIES     (Theory Graph)

alignment     alist_tree     alist     arithmetic     ASCIInumbers     bag     basicSize     basis_emit     bft     binary_ieee     bisimulation     bitArith     bitstring     bit     blast     bool     borel     byte     cardinal     coalgAxioms     Coder     combin     comparison     complex     ConseqConv     container     countable_types     cv_prim     cv_rep     cv_std     cv_type     cv     Decode     DeepSyntax     defCNF     derivative     dft     dirGraph     divides     emitOrdinal     Encode     EncodeVar     enumeral     errorStateMonad     EVAL_canonical     EVAL_numRing     EVAL_quote     EVAL_ringNorm     EVAL_ring     EVAL_semiring     extended_emit     extreal_base     extreal     fcp     finite_map     finite_set     fixedPoint     float     fmapal     fmaptree     frac     gcdset     gcd     HolSmt     hrat     hreal     ieee     ind_type     indexedLists     inftree     int_arith     int_bitwise     integer_word     integerRing     integer     integral     integration     intExtension     intreal     intto     iterate     itreeTau     itree     lbtree     lebesgue     lift_ieee     lift_machine_ieee     lifting     lim     listRange     list     llist     logroot     ltree     machine_ieee     marker     martingale     measure     mergesort     metric     nets     nlist     normalForms     numeral_bit     numeral     numpair     numposrep     num     Omega_Automata     Omega     one     option     ordinalNotation     ordinal     ordNotationSemantics     pair     Past_Temporal_Logic     path     patricia_casts     patricia     patternMatches     permutes     poly     poset     powser     pred_set     prim_rec     primeFactor     probability     quantHeuristics     quotient     ratRing     rat     readerMonad     real_borel     real_of_rat     real_sigma     real_topology     realax     real     relation     res_quan     rich_list     sat     seq     set_relation     sigma_algebra     simpleSetCat     sorting     sptree     state_transformer     string_encoding     string_num     string     sum_num     sum     tc     Temporal_Logic     ternaryComparisons     topology     toto     transc     transfer     update     util_prob     veblen     wellorder     while     words    

STRUCTURES

Abbrev     abstraction     Absyn     AC     AC_Sort     AList     AncestryData     Arbint     Arbintcore     Arbnum     Arbnumcore     Arbrat     Arith     Arith_cons     Arithconv     AssembleHolindexParser     base_tokens     BasicProvers     Boolconv     BoolExtractShared     boolpp     BoundedRewrites     Cache     Canon     Canon_Port     CharSet     clauses     Coding     combinpp     Compute     compute_rules     Cond_rewr     Cond_rewrite     ConseqConv     ConstMapML     Conv     Cooper     CooperCore     CooperMath     CooperShell     CooperThms     Count     CSimp     DataSize     Datatype     DB     DecimalFractionPP     def_cnf     defCNF     DefinitionDoc     Defn     DefnBase     DefnBaseCore     Dep     dep_rewrite     Diff     DiskThms     Drule     Dynarray     EmitML     EmitTeX     Encode     enumTacs     EnumType     errormonad     EVAL_quote     EvalRef     Exists_arith     Exn     FCNet     Feedback     FinalNet     FinalTag     FinalTerm     FinalThm     FinalType     FlagDB     fmapalTacs     folMapping     folTools     fracUtils     FullUnify     Gen_arith     GenPolyCanon     Globals     goalStack     goalTree     GrammarAncestry     GrammarDeltas     GrammarSpecials     Grobner     hhExportFof     hhExportSexpr     hhExportTf0     hhExportTf1     hhExportTh0     hhExportTh1     hhReconstruct     hhTptp     hhTranslate     History     Ho_Net     Ho_Rewrite     Hol_pp     HOLdict     holindexData     HolKernelDoc     HOLPP     HOLset     HOLsexp     HOLsexp_parser     HOLtokens     holyHammer     hurdUtils     ImplicitGraph     ind_types     IndDefRules     Induction     InductiveDefinition     Instance     Int_extra     IntDP_Munge     Intmap     intReduce     Intset     inttoTacs     jrhCore     jrhTactics     jrhUtils     KernelSig     Lexis     Lib     Lift     ListConv1     Literal     locn     LVTermNet     Manager     match_goal     matchTools     MD5     metisTools     minisatProve     mlFeature     mlibArbint     mlibArbnum     mlibCanon     mlibClause     mlibClauseset     mlibHeap     mlibKernel     mlibLiteralnet     mlibMatch     mlibMeson     mlibMeter     mlibMetis     mlibModel     mlibMultiset     mlibOmega     mlibOmegaint     mlibParser     mlibPatricia     mlibPortable     mlibResolution     mlibRewrite     mlibSolver     mlibStream     mlibSubst     mlibSubsume     mlibSupport     mlibTerm     mlibTermnet     mlibTermorder     mlibThm     mlibTptp     mlibUnits     mlibUseful     mlMatrix     mlNearestNeighbor     mlNeuralNetwork     mlReinforce     MLstring     mlTacticData     mlThmData     mlTreeNeuralNetwork     monadsyntax     mp_then     mungeTools     Mutual     Net     newtypeTools     Nonce     Norm_arith     Norm_bool     Norm_ineqs     normalForms     Normalizer     Num_conv     NumRelNorms     OldAbbrevTactics     OldPP     Omega     OmegaMath     OmegaMLShadow     OmegaShell     OmegaSimple     OmegaSymbolic     Opening     OpenTheoryCommon     OpenTheoryMap     OpenTheoryReader     optmonad     Overload     PairedLambda     PairRules     pairTools     Parmap     parmonadsyntax     Parse     Parse_support     parse_term     parse_type     ParseDatatype     ParseExtras     parsePMATCH     PEGParse     PFset_conv     PGspec     PIntMap     Pmatch     PmatchHeuristics     Portable     PPBackEnd     PrecAnalysis     pred_setpp     PreListEncode     Prenex     Preterm     Pretype     Prim_rec     Profile     ProvideUnicode     psBigSteps     PSet_ind     psMCTS     psMinimize     psTermGen     Psyntax     Q     qbuf     quantHeuristicsLibAbbrev     quantHeuristicsLibBase     quantHeuristicsLibFunRemove     quantHeuristicsLibParameters     quantHeuristicsLibSimple     quantHeuristicsTools     quotient     Random     Rationals     ratReduce     ratUtils     readermonad     RealArith     RealField     RecordType     Redblackmap     Redblackset     res_quanTools     resolve_then     Rewrite     RJBConv     Rsyntax     Rules     RW     Sanity     satConfig     Satisfy     schneiderUtils     seq     seqmonad     Sequence     SHA1     SHA1_ML     SharingTables     simpfrag     smlExecScripts     smlExecute     smlInfix     smlLexer     smlOpen     smlParallel     smlParser     smlPrettify     smlRedirect     smlTimeout     smpp     Sol_ranges     Solve     Solve_ineqs     sptreepp     Sref     stmonad     Streams     stringfindreplace     Sub_and_cond     Subst     Sup_Inf     Susp     Systeml     Tactic     Tactical     tacticToe     Tag     tcTacs     Term     Term_coeffs     term_grammar     term_pp     term_pp_utils     term_tactic     term_tokens     TermParse     testutils     TexTokenMap     Theorems     Theory     TheoryGraph     TheoryPP     TheoryReader     Thm     Thm_cont     Thm_convs     ThmAttribute     ThmSetData     ThyDataSexp     TotalDefn     totoTacs     Trace     Traverse     Travrules     tttEval     tttLearn     tttRecord     tttSearch     tttSetup     tttToken     tttTrain     tttUnfold     Type     type_grammar     type_pp     type_tokens     TypeBase     TypeBasePure     TypeNet     UC_ASCII_Encode     UnicodeChars     Unify     Unittest     UniversalType     Unwind     Uref     UTF8     UTF8Set     wfrecUtils     wordspp    

SYNTAX

alignment     ASCIInumbers     bag     basicSize     binary_ieee     bitstring     bit     bool     combin     Cooper     cv     fcp     finite_map     frac     integer_word     intreal     int     list     machine_ieee     marker     numposrep     num     one     option     pair     patricia_casts     patricia     patternMatches     pred_set     rat     real     relation     rich_list     sorting     sptree     state_transformer     string     sum     transc     update     words    

SIMPLIFICATION SETS

bag     bool     combin     Datatype     extreal     indexedLists     int     list     num     option     pair     pred_set     pure     real     rich_list     Satisfy     string     sum    

IDENTIFIERS    THEORY BINDINGS