CookBook/Intro.thy
changeset 12 2f1736cb8f26
parent 11 733614e236a3
child 42 cd612b489504
equal deleted inserted replaced
11:733614e236a3 12:2f1736cb8f26
    37   concepts and some of the interfaces. 
    37   concepts and some of the interfaces. 
    38 
    38 
    39   \item[The Isabelle Reference Manual] is an older document that used
    39   \item[The Isabelle Reference Manual] is an older document that used
    40   to be the main reference at a time when all proof scripts were written 
    40   to be the main reference at a time when all proof scripts were written 
    41   on the ML level. Many parts of this manual are outdated now, but some 
    41   on the ML level. Many parts of this manual are outdated now, but some 
    42   parts, mainly the chapters on tactics, are still useful.
    42   parts, particularly the chapters on tactics, are still useful.
    43   \end{description}
    43   \end{description}
    44 
    44 
    45   Then of ourse there is:
    45   Then of course there is:
    46 
    46 
    47   \begin{description}
    47   \begin{description}
    48   \item[The code] is of course the ultimate reference for how
    48   \item[The code] is of course the ultimate reference for how
    49   things really work. Therefore you should not hesitate to look at the
    49   things really work. Therefore you should not hesitate to look at the
    50   way things are actually implemented. More importantly, it is often
    50   way things are actually implemented. More importantly, it is often