Session HOL-Mirabelle-ex
View
theory dependencies
Theories
HOL-Analysis.Inner_Product