HOL Reference Page

LIBRARIES

ASCIInumbers     bag     bagSimple     binary_ieee     bit     bitstring     blast     boss     combin     compute     cong     fcp     finite_map     flookup     frac     hol88     HolQbf     HolSat     HolSmt     IndDef     integer_word     integerRing     intExtension     int     isqrt     list     lite     machine_ieee     marker     meson     metis     num     numposrep     numRing     option     pair     patricia_casts     patricia     perm     pred_set     proofManager     quantHeuristics     rat     ratRing     real     reduce     refute     res_quan     ring     simp     sptree     string     taut     temporal     unwind     update     words    

THEORIES     (Theory Graph)

alist     arithmetic     ASCIInumbers     bag     basicSize     basis_emit     binary_ieee     bitstring     bit     blast     bool     canonical     Coder     combin     complex     ConseqConv     container     Decode     DeepSyntax     defCNF     divides     Encode     EncodeVar     enumeral     extreal     fcp     finite_map     fixedPoint     float     fmapal     fmaptree     frac     gcdset     gcd     HolSmt     hrat     hreal     ieee     ind_type     inftree     int_arith     int_bitwise     integer_word     integerRing     integer     integral     intExtension     intreal     intto     lbtree     lebesgue     lim     listRange     list     llist     logroot     machine_ieee     marker     measure     mergesort     nets     normalForms     numeral_bit     numeral     numpair     numposrep     numRing     num     Omega_Automata     Omega     one     operator     option     pair     Past_Temporal_Logic     path     patricia_casts     patricia     poly     poset     powser     pred_set     prelim     prim_rec     primeFactor     probability     quantHeuristics     quote     quotient_list     quotient_option     quotient_pair     quotient_pred_set     quotient_sum     quotient     ratRing     rat     real_sigma     realax     real     relation     res_quan     rich_list     ringNorm     ring     sat     semi_ring     seq     set_relation     sorting     sptree     state_option     state_transformer     string_num     stringDict     string     sum_num     sum     tc     Temporal_Logic     topology     toto     transc     update     util_prob     while     words     wot    

STRUCTURES

Abbrev     abstraction     Absyn     AC     AC_Sort     Arbint     Arbintcore     Arbnum     Arbnumcore     Arbrat     Arith     Arith_cons     Arithconv     AssembleDiskFiles     AssembleHolindexParser     base_tokens     BasicProvers     Boolconv     BoolExtractShared     BoundedRewrites     Cache     Canon     Canon_Port     CharSet     clauses     Coding     compute_rules     Cond_rewr     Cond_rewrite     ConseqConv     ConstMapML     Conv     Cooper     CooperCore     CooperMath     CooperShell     CooperThms     CoreKernel     Count     CSimp     DataSize     Datatype     DB     DecimalFractionPP     defCNF     Defn     DefnBase     dep_rewrite     Diff     DiskFilesHeader     DiskThms     Drule     Dynarray     EmitML     EmitTeX     Encode     enumTacs     EnumType     EquivType     errormonad     EvalRef     Exists_arith     Feedback     FinalTag     FinalTerm     FinalThm     FinalType     fmapalTacs     folMapping     folTools     fp     fracUtils     Gen_arith     GenPolyCanon     Globals     goalStack     goalTree     GrammarSpecials     History     Ho_Net     Ho_Rewrite     Hol_pp     HOLgrammars     holindexData     HolKernelDoc     HOLPP     HOLset     HOLtokens     ind_types     IndDefRules     Induction     InductiveDefinition     Instance     Int_extra     IntDP_Munge     Intmap     intReduce     Intset     inttoTacs     jbUtils     jrhCore     jrhTactics     jrhUtils     KernelSig     KernelTypes     lcsymtacs     Lexis     Lib     Lift     ListConv1     Literal     locn     LVTermNet     Manager     matchTools     MD5     metisTools     minisatProve     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     MLstring     monadsyntax     mungeTools     Mutual     Net     newtypeTools     Nonce     Norm_arith     Norm_bool     Norm_ineqs     normalForms     Num_conv     NumRelNorms     OldAbbrevTactics     Omega     OmegaMath     OmegaMLShadow     OmegaShell     OmegaSimple     OmegaSymbolic     Opening     Opentheory     OpenTheoryCommon     OpenTheoryMap     optmonad     Overload     PairedLambda     PairRules     pairTools     parmonadsyntax     Parse     Parse_support     parse_term     parse_type     ParseDatatype     ParseExtras     PEGParse     PFset_conv     PGspec     PIntMap     Pmatch     PmatchHeuristics     Portable     PPBackEnd     PreListEncode     Prenex     Preterm     Pretype     Prim_rec     Profile     ProvideUnicode     PSet_ind     Psyntax     Q     QbfConv     qbuf     quantHeuristicsLibAbbrev     quantHeuristicsLibBase     quantHeuristicsLibFunRemove     quantHeuristicsLibParameters     quantHeuristicsTools     quotient     Random     Rationals     ratUtils     Raw     RealArith     RecordType     Redblackmap     Redblackset     res_quanTools     Rewrite     RJBConv     Rsyntax     Rules     RW     Sanity     satConfig     Satisfy     schneiderUtils     seq     seqmonad     Sequence     SharingTables     simpfrag     smpp     Sol_ranges     Solve     Solve_ineqs     stmonad     Streams     Sub_and_cond     Subst     Sup_Inf     Susp     Systeml     Tactic     Tactical     Tag     tcTacs     Term     Term_coeffs     term_grammar     term_pp     term_pp_utils     term_tokens     TermCoding     TermParse     testutils     TexTokenMap     Theorems     Theory     TheoryPP     Thm     Thm_cont     Thm_convs     ThmSetData     TotalDefn     totoTacs     Trace     Traverse     Travrules     Type     type_grammar     type_pp     type_tokens     TypeBase     TypeBasePure     TypeNet     UnicodeChars     Unify     UniversalType     Unwind     UTF8     UTF8Set     wfrecUtils    

SYNTAX

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

SIMPLIFICATION SETS

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

THEORY BINDINGS