With-Type – Poor man's dependent types

The type system of Isabelle/HOL does not support dependent types or arbitrary quantification over types. We introduce a system to mimic dependent types and existential quantification over types in limited circumstances at the top level of theorems.