summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | lcp |

Tue, 03 May 1994 10:40:24 +0200 | |

changeset 348 | 1f5a94209c97 |

parent 347 | cd41a57221d0 |

child 349 | 0ddc495e8b83 |

post-CRC corrections

doc-src/Intro/advanced.tex | file | annotate | diff | comparison | revisions | |

doc-src/Intro/intro.tex | file | annotate | diff | comparison | revisions |

--- a/doc-src/Intro/advanced.tex Mon May 02 12:34:56 1994 +0200 +++ b/doc-src/Intro/advanced.tex Tue May 03 10:40:24 1994 +0200 @@ -546,7 +546,7 @@ negate :: "signal => signal" \end{ttbox} -\subsection{Infix and Mixfix operators} +\subsection{Infix and mixfix operators} \index{infixes}\index{examples!of theories} Infix or mixfix syntax may be attached to constants. Consider the @@ -675,8 +675,8 @@ \index{examples!of theories} \begin{ttbox} BoolNat = Arith + -types bool,nat -arities bool,nat :: arith +types bool nat +arities bool, nat :: arith consts Suc :: "nat=>nat" \ttbreak rules add0 "0 + n = n::nat"

--- 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}