equal
deleted
inserted
replaced
34 (*>*) |
34 (*>*) |
35 |
35 |
36 section {* Introduction *} |
36 section {* Introduction *} |
37 |
37 |
38 text {* |
38 text {* |
39 {\hfill quote by Larry}\bigskip |
39 \begin{flushright} |
|
40 {\em ``Not using a [quotient] package has its advantages: we do not have to\\ |
|
41 collect all the theorems we shall ever want into one giant list;''}\\ |
|
42 Paulson \cite{Paulson06} |
|
43 \end{flushright}\smallskip |
40 |
44 |
41 \noindent |
45 \noindent |
42 Isabelle is a generic theorem prover in which many logics can be implemented. |
46 Isabelle is a generic theorem prover in which many logics can be implemented. |
43 The most widely used one, however, is |
47 The most widely used one, however, is |
44 Higher-Order Logic (HOL). This logic consists of a small number of |
48 Higher-Order Logic (HOL). This logic consists of a small number of |