Up to index of Isabelle/HOL/HOL4
(* Title: HOL/Import/HOL/HOL4.thy Author: Sebastian Skalberg, TU Muenchen*)theory HOL4 imports HOL4Vec HOL4Word32 HOL4Real beginend