| changeset 12621 | 48cafea0684b |
| parent 12618 | 43a97a2155d0 |
| child 12879 | 8e1cae1de136 |
--- a/doc-src/IsarRef/intro.tex Thu Jan 03 17:01:59 2002 +0100 +++ b/doc-src/IsarRef/intro.tex Thu Jan 03 17:48:02 2002 +0100 @@ -265,6 +265,8 @@ \subsection{How to write Isar proofs anyway?}\label{sec:isar-howto} +%FIXME tune + This is one of the key questions, of course. Isar offers a rather different approach to formal proof documents than plain old tactic scripts. Experienced users of existing interactive theorem proving systems may have to learn