HOL Reference Page

LIBRARIES

bag     boss     compute     fcp     goalstack     hol88     holCheck     HolSat     IndDef     integerRing     int     list     lite     meson     num     numRing     option     pair     pred_set     prob     rat     ratRing     real     reduce     res_quan     ring     simp     string     taut     temporal     unwind     word     words    

THEORIES     (Theory Graph)

arithmetic     bag     bit     boolean_sequence     bool     bword_arith     bword_bitop     bword_num     canonical     Coder     combin     container     Decode     defCNF     divides     Encode     EncodeVar     fcp     finite_map     fixedPoint     float     fxp     gcd     hrat     hreal     ieee     ind_type     integerRing     integer     lim     list     llist     MachineTransition     nets     numeral     numRing     num     Omega_Automata     one     operator     option     pair     Past_Temporal_Logic     path     poly     powser     pred_set     prelim     prim_rec     prob_algebra     prob_canon     prob_extra     prob_indep     prob_pseudo     prob_uniform     prob     quote     rat     realax     real     relation     res_quan     rich_list     ringNorm     ring     semi_ring     seq     sorting     state_transformer     string     sum     Temporal_Logic     topology     transc     while     word_base     word_bitop     word_num     words     word    

STRUCTURES

Abbrev     Absyn     AC     Arbint     Arbnum     BasicProvers     Canon     Canon_Port     Conv     Cooper     Count     Datatype     DB     defCNF     Definition     Defn     DefnBase     DerivedBddRules     Drule     EquivType     Feedback     Globals     Ho_Net     Ho_Rewrite     Hol_pp     ind_types     IndDefRules     InductiveDefinition     jrhTactics     Lexis     Lib     Net     PairedLambda     PairRules     pairTools     Parse     Portable     Preterm     Prim_rec     PrimitiveBddRules     PrintBdd     Psyntax     Q     RealArith     RecordType     Rewrite     Rsyntax     SingleStep     Systeml     Tactic     Tactical     Tag     Term     Theory     Thm     Thm_cont     TotalDefn     Type     TypeBase     TypeBasePure     Varmap    

SYNTAX

bag     bool     combin     int     list     num     option     pair     pred_set     rat     string     sum     words    

SIMPLIFICATION SETS

bag     bool     list     num     option     pair     pred_set     real     string     sum    

IDENTIFIERS    THEORY BINDINGS