equal
deleted
inserted
replaced
49 calculus, higher-order logic, Zermelo-Fraenkel set theory~\cite{suppes72}, |
49 calculus, higher-order logic, Zermelo-Fraenkel set theory~\cite{suppes72}, |
50 a version of Constructive Type Theory~\cite{nordstrom90}, several modal |
50 a version of Constructive Type Theory~\cite{nordstrom90}, several modal |
51 logics, and a Logic for Computable Functions~\cite{paulson87}. Several |
51 logics, and a Logic for Computable Functions~\cite{paulson87}. Several |
52 experimental logics are being developed, such as linear logic. |
52 experimental logics are being developed, such as linear logic. |
53 |
53 |
54 \centerline{\epsfbox{Isa-logics.eps}} |
54 \centerline{\epsfbox{gfx/Isa-logics.eps}} |
55 |
55 |
56 |
56 |
57 \section*{How to read this book} |
57 \section*{How to read this book} |
58 Isabelle is a complex system, but beginners can get by with a few commands |
58 Isabelle is a complex system, but beginners can get by with a few commands |
59 and a basic knowledge of how Isabelle works. Some knowledge of |
59 and a basic knowledge of how Isabelle works. Some knowledge of |