| changeset 7987 | d9aef93c0e32 |
| parent 7981 | 5120a2a15d06 |
| child 8508 | 76d8d8aab881 |
--- a/doc-src/IsarRef/intro.tex Sat Oct 30 20:41:30 1999 +0200 +++ b/doc-src/IsarRef/intro.tex Sun Oct 31 15:20:35 1999 +0100 @@ -149,7 +149,7 @@ \end{tabular} \end{center} -See \texttt{HOL/Isar_examples} for a collection of introductory examples. +See \texttt{HOL/Isar_examples} for a collection of introductory examples, and \texttt{HOL/HOL-Real/HahnBanach} is a big mathematics application. Apart from browsable HTML sources, both sessions provide actual documents (in PDF).