equal
deleted
inserted
replaced
42 automatically visible. To avoid name clashes, identifiers can be qualified by |
42 automatically visible. To avoid name clashes, identifiers can be qualified by |
43 theory names as in \texttt{T.f} and \texttt{B.f}. HOL's theory library is |
43 theory names as in \texttt{T.f} and \texttt{B.f}. HOL's theory library is |
44 available online at |
44 available online at |
45 |
45 |
46 \begin{center}\small |
46 \begin{center}\small |
47 \begin{tabular}{l} |
47 \url{http://isabelle.in.tum.de/library/} |
48 \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/} \\ |
|
49 \url{http://isabelle.in.tum.de/library/} \\ |
|
50 \end{tabular} |
|
51 \end{center} |
48 \end{center} |
52 |
49 |
53 and is recommended browsing. |
50 and is recommended browsing. |
54 \begin{warn} |
51 \begin{warn} |
55 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 |