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

author | paulson |

Tue, 18 Dec 2001 16:44:00 +0100 | |

changeset 12540 | a5604ff1ef4e |

parent 12539 | 368414099877 |

child 12541 | c6e454ec501c |

minor suggestions from Markus

--- a/doc-src/TutorialI/Protocol/protocol.tex Tue Dec 18 16:14:56 2001 +0100 +++ b/doc-src/TutorialI/Protocol/protocol.tex Tue Dec 18 16:44:00 2001 +0100 @@ -488,7 +488,9 @@ it is known to the spy. Intuitively, it holds because honest agents always choose fresh values as nonces; only the spy might reuse a value, and he doesn't know this particular value. The proof script is short: -induction, simplification, \isa{blast}. +induction, simplification, \isa{blast}. The first line uses the rule +\isa{rev_mp} to prepare the induction by moving two assumptions into the +induction formula. \begin{isabelle} \isacommand{lemma}\ no_nonce_NS1_NS2:\isanewline \ \ \ \ "\isasymlbrakk Crypt\ (pubK\ C)\ \isasymlbrace NA',\ Nonce\

--- a/doc-src/TutorialI/Rules/rules.tex Tue Dec 18 16:14:56 2001 +0100 +++ b/doc-src/TutorialI/Rules/rules.tex Tue Dec 18 16:44:00 2001 +0100 @@ -851,8 +851,8 @@ An alternative to \isa{rule_tac} is to use \isa{rule} with a theorem modified using~\isa{of}, described in -{\S}\ref{sec:forward} below. An advantage of \isa{rule_tac} is that the -instantiations may refer to +{\S}\ref{sec:forward} below. But \isa{rule_tac}, unlike \isa{of}, can +express instantiations that refer to \isasymAnd-bound variables in the current subgoal.% \index{substitution|)} @@ -1260,8 +1260,9 @@ A definite description is traditionally written $\iota x. P(x)$. It denotes the $x$ such that $P(x)$ is true, provided there exists a unique such~$x$; otherwise, it returns an arbitrary value of the expected type. -Isabelle uses \sdx{THE} for the Greek letter~$\iota$. (The -traditional notation could be provided, but it is not legible on screen.) +Isabelle uses \sdx{THE} for the Greek letter~$\iota$. + +%(The traditional notation could be provided, but it is not legible on screen.) We reason using this rule, where \isa{a} is the unique solution: \begin{isabelle} @@ -2301,8 +2302,9 @@ A postfixed question mark~(\isa?)\index{*"? (tactical)} expresses zero or one repetitions of a method. It can also be viewed as the choice between executing a -method and doing nothing. It is useless at top level but may be valuable within -other control structures.% +method and doing nothing. It is useless at top level but can be valuable +within other control structures; for example, +\isa{($m$+)?} performs zero or more repetitions of method~$m$.% \index{tacticals|)}

--- a/doc-src/TutorialI/Sets/sets.tex Tue Dec 18 16:14:56 2001 +0100 +++ b/doc-src/TutorialI/Sets/sets.tex Tue Dec 18 16:44:00 2001 +0100 @@ -387,9 +387,8 @@ \cdx{UNION} and \cdx{INTER}\@. The internal constant for $\varepsilon x.P(x)$ is~\cdx{Eps}. -We have only scratched the surface of Isabelle/HOL's set theory. -Hundreds of theorems are proved in theory \isa{Set} and its -descendants. +We have only scratched the surface of Isabelle/HOL's set theory, which provides +hundreds of theorems for your use. \subsection{Finiteness and Cardinality} @@ -1070,6 +1069,5 @@ is perhaps the best-known concept defined as a greatest fixed point. Exhibiting a bisimulation to prove the equality of two agents in a process algebra is an example of coinduction. -The coinduction rule can be strengthened in various ways; see -theory \isa{Gfp} for details. +The coinduction rule can be strengthened in various ways. \index{fixed points|)}