equal
deleted
inserted
replaced
147 \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/} \\ |
147 \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/} \\ |
148 \url{http://isabelle.in.tum.de/library/} \\ |
148 \url{http://isabelle.in.tum.de/library/} \\ |
149 \end{tabular} |
149 \end{tabular} |
150 \end{center} |
150 \end{center} |
151 |
151 |
152 See \texttt{HOL/Isar_examples} for a collection of introductory examples. |
152 See \texttt{HOL/Isar_examples} for a collection of introductory examples, and |
153 \texttt{HOL/HOL-Real/HahnBanach} is a big mathematics application. Apart from |
153 \texttt{HOL/HOL-Real/HahnBanach} is a big mathematics application. Apart from |
154 browsable HTML sources, both sessions provide actual documents (in PDF). |
154 browsable HTML sources, both sessions provide actual documents (in PDF). |
155 |
155 |
156 %%% Local Variables: |
156 %%% Local Variables: |
157 %%% mode: latex |
157 %%% mode: latex |