7 citations · 7 across the 1 of their papers we have counts for
1 paper
Tobias Nipkow, Simon Roßkopf
Isabelle is a generic theorem prover with a fragment of higher-order logic as a metalogic for defining object logics. Isabelle also provides proof terms. We formalize this metalogi…