Lines Matching defs:of
12 explicitly concerned with computation and capable of expressing
16 A diverse collection of logics --- type theories, process calculi,
21 A {\bf generic} theorem prover is one that supports a variety of logics.
23 \cite{dawson90,mural,sawamura92}. Most of them work by implementing a
25 distinctive feature is its representation of logics within a fragment of
26 higher-order logic, called the meta-logic. The proof theory of
30 Felty's~\cite{felty93} use of $\lambda$Prolog to implement logics.
47 The diagram below illustrates some of the logics distributed with Isabelle.
50 a version of Constructive Type Theory~\cite{nordstrom90}, several modal
59 and a basic knowledge of how Isabelle works. Some knowledge of
68 \item {\em Introduction to Isabelle\/} describes the basic features of
72 present on-line sessions of increasing difficulty. It also explains how
86 a couple of chapters from {\em Introduction to Isabelle}, then try some
93 \section*{Releases of Isabelle}
95 higher-order meta-logic with an improved treatment of quantifiers. The
103 better support for inductive definitions, some means of recording proofs, a
114 Please notify me of any errors you find in this book.
119 He also arranged for several of his students to help. Carsten Clasohm
123 Nipkow and his students wrote much of the documentation underlying this
124 book. Nipkow wrote the first versions of \S\ref{sec:defining-theories},