HOL Reference Page

LIBRARIES

bag     boss     compute     fcp     hol88     HolSat     IndDef     integerRing     int     list     lite     marker     meson     num     numRing     option     pair     patricia_casts     patricia     perm     pred_set     prob     proofManager     quantHeuristics     rat     ratRing     real     reduce     res_quan     ring     simp     string     taut     temporal     unwind     words    

THEORIES     (Theory Graph)

arithmetic     bag     bit     boolean_sequence     bool     canonical     Coder     combin     container     Decode     divides     Encode     EncodeVar     fcp     finite_map     fixedPoint     float     gcd     hrat     hreal     ieee     ind_type     integer_word     integerRing     integer     lim     list     llist     nets     numeral     numRing     num     Omega_Automata     one     operator     option     pair     Past_Temporal_Logic     path     patricia_casts     patricia     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     words    

STRUCTURES

Abbrev     Absyn     AC     Arbint     Arbnum     BasicProvers     Canon     Canon_Port     ConseqConv     Conv     Cooper     Count     Datatype     DB     Definition     Defn     DefnBase     Drule     EmitML     EmitTeX     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     Psyntax     Q     RealArith     RecordType     Rewrite     Rsyntax     SingleStep     Systeml     Tactic     Tactical     Tag     Term     Theory     Thm     Thm_cont     TotalDefn     Type     TypeBase     TypeBasePure    

SYNTAX

bag     bit     bool     combin     int     list     marker     num     option     pair     patricia_casts     patricia     pred_set     rat     string     sum     words    

SIMPLIFICATION SETS

bag     bool     list     num     option     pair     pred_set     real     string     sum    

THEORY BINDINGS