summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

doc-src/Intro/intro.tex

changeset 348 | 1f5a94209c97 |

parent 311 | 3fb8cdb32e10 |

child 873 | 0cfc734e3dbd |

--- a/doc-src/Intro/intro.tex Mon May 02 12:34:56 1994 +0200 +++ b/doc-src/Intro/intro.tex Tue May 03 10:40:24 1994 +0200 @@ -43,7 +43,7 @@ \begin{itemize} \item first-order logic, constructive and classical versions \item higher-order logic, similar to that of Gordon's {\sc -hol}~\cite{gordon88a} +hol}~\cite{mgordon-hol} \item Zermelo-Fraenkel set theory~\cite{suppes72} \item an extensional version of Martin-L\"of's Type Theory~\cite{nordstrom90} \item the classical first-order sequent calculus, {\sc lk} @@ -68,7 +68,7 @@ texts~\cite{galton90,reeves90}. \index{LCF} -{\sc lcf}, developed by Robin Milner and colleagues~\cite{gordon79}, is an +{\sc lcf}, developed by Robin Milner and colleagues~\cite{mgordon79}, is an ancestor of {\sc hol}, Nuprl, and several other systems. Isabelle borrows ideas from {\sc lcf}: formulae are~\ML{} values; theorems belong to an abstract type; tactics and tacticals support backward proof. But {\sc lcf} @@ -76,15 +76,6 @@ by terms. You may find my other writings~\cite{paulson87,paulson-handbook} helpful in understanding the relationship between {\sc lcf} and Isabelle. -Isabelle does not keep a record of inference steps. Each step is checked -at run time to ensure that theorems can only be constructed by applying -inference rules. An Isabelle proof typically involves hundreds of -primitive inferences, and would be unintelligible if displayed. -Discarding proofs saves vast amounts of storage. But can Isabelle be -trusted? If desired, object-logics can be formalized such that each -theorem carries a proof term, which could be checked by another program. -Proofs can also be traced. - \index{Isabelle!release history} Isabelle was first distributed in 1986. The 1987 version introduced a higher-order meta-logic with an improved treatment of quantifiers. The 1988 version added limited polymorphism and @@ -142,7 +133,7 @@ \include{advanced} \bibliographystyle{plain} \small\raggedright\frenchspacing -\bibliography{string,atp,funprog,general,logicprog,theory} +\bibliography{string,atp,funprog,general,logicprog,isabelle,theory} \input{intro.ind} \end{document}