40 newly introduced concepts (types, functions etc). The \texttt{B}$@i$ are the |
40 newly introduced concepts (types, functions etc). The \texttt{B}$@i$ are the |
41 direct \textbf{parent theories}\indexbold{parent theory} of \texttt{T}. |
41 direct \textbf{parent theories}\indexbold{parent theory} of \texttt{T}. |
42 Everything defined in the parent theories (and their parents \dots) is |
42 Everything defined in the parent theories (and their parents \dots) is |
43 automatically visible. To avoid name clashes, identifiers can be qualified by |
43 automatically visible. To avoid name clashes, identifiers can be qualified by |
44 theory names as in \texttt{T.f} and \texttt{B.f}. HOL's theory library is |
44 theory names as in \texttt{T.f} and \texttt{B.f}. HOL's theory library is |
45 available online at \verb$http://www.in.tum.de/~isabelle/library/HOL/$ and is |
45 available online at |
46 recommended browsing. |
46 \begin{ttbox} |
|
47 http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/HOL/ |
|
48 http://isabelle.in.tum.de/library/HOL/ |
|
49 \end{ttbox} |
|
50 and is recommended browsing. |
47 \begin{warn} |
51 \begin{warn} |
48 HOL contains a theory \ttindexbold{Main}, the union of all the basic |
52 HOL contains a theory \ttindexbold{Main}, the union of all the basic |
49 predefined theories like arithmetic, lists, sets, etc.\ (see the online |
53 predefined theories like arithmetic, lists, sets, etc.\ (see the online |
50 library). Unless you know what you are doing, always include \texttt{Main} |
54 library). Unless you know what you are doing, always include \texttt{Main} |
51 as a direct or indirect parent theory of all your theories. |
55 as a direct or indirect parent theory of all your theories. |