The HOL4 types, constants, and theorems can be found easily in the the
theories: In Isabelle, they will normally just be called
<library>.<name>
. For example, the theorem
REAL_LT_RDIV
found in the HOL4 library real
can be accessed as real.REAL_LT_RDIV
.
Sometimes, you won't find a certain type, constant, or theorem in the Isabelle theory. Then what? First, make sure the HOL4 library has even been ported (see the table below). If it has, then one of several things can have happened:
NIL
of the list
library is found as
List.list.Nil
in Isabelle.
word32
library, for example, clashes with
Isabelle's meta-equality, and has therefore been renamed to
EQUIV
<library>.imp
. The information in the
imp
file might allow you to figure out what actually
happened.
HOL4Base | arithmetic bool combin divides hrat hreal ind_type list marker num numeral one operator option pair pred_set prime prim_rec relation rich_list sum |
HOL4Real | lim nets poly powser real realax seq topology transc |
HOL4Prob | boolean_sequence prob prob_algebra prob_canon prob_extra prob_indep prob_pseudo prob_uniform state_transformer |
HOL4Vec | bword_arith bword_bitop bword_num res_quan word_base word_bitop word_num |
HOL4Word32 | bits word32 |