I want to see the definitions in the vector spaces theory file of the Isabelle/HOL distribution. This thread of the Isabelle's mailing list explains how to do so with the command: isabelle make HOL-Base
.
I am working under Windows 10. I guess the above command is meant for Linux. How can I get the same effect in my system?
Try to start Isabelle from the command line with isabelle jedit -l Pure
(command-line tools are invoked through Isabelle2018\Cygwin-Terminal.bat
under Windows). Now Isabelle/Pure is used as the base image instead of Isabelle/HOL. Next load the theory file you want to check from the Isabelle installation directory (HOL stuff is under <isabelle-dir>/src/HOL
)