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

author | lcp |

Fri, 26 Nov 1993 12:31:48 +0100 | |

changeset 156 | ab4dcb9285e0 |

parent 155 | f58571828c68 |

child 157 | 8258c26ae084 |

Corrected errors found by Marcus Wenzel.

--- a/doc-src/Intro/advanced.tex Thu Nov 25 19:09:43 1993 +0100 +++ b/doc-src/Intro/advanced.tex Fri Nov 26 12:31:48 1993 +0100 @@ -274,7 +274,7 @@ \medskip Again, there is a simpler way of conducting this proof. The -\ttindex{goalw} command starts unfolds definitions in the premises, as well +\ttindex{goalw} command unfolds definitions in the premises as well as the conclusion: \begin{ttbox} val [major,minor] = goalw FOL.thy [not_def] @@ -564,9 +564,14 @@ \begin{ttbox} If :: "[o,o,o] => o" ("if _ then _ else _" [100,0,0] 99) \end{ttbox} -defines a conditional whose first argument cannot be a conditional because it -must have a precedence of at least 100. Precedences only apply to -mixfix syntax: we may write $If(If(P,Q,R),S,T)$. +defines concrete syntax for a +conditional whose first argument cannot have the form $if~P~then~Q~else~R$ +because it must have a precedence of at least~100. Since expressions put in +parentheses have maximal precedence, we may of course write +\begin{quote} +\it if (if P then Q else R) then S else T +\end{quote} +Conditional expressions can also be written using the constant {\tt If}. Binary type constructors, like products and sums, may also be declared as infixes. The type declaration below introduces a type constructor~$*$ with @@ -1189,11 +1194,6 @@ {\out rev(a : b : c : d : Nil, d : c : b : a : Nil)} {\out No subgoals!} \end{ttbox} -Although Isabelle is much slower than a {\sc Prolog} system, many -Isabelle tactics exploit logic programming techniques. For instance, the -simplification tactics prove subgoals of the form $t=\Var{x}$, rewriting~$t$ -and placing the normalised result in~$\Var{x}$. -% Local Variables: -% mode: latex -% TeX-master: t -% End: +Although Isabelle is much slower than a {\sc Prolog} system, Isabelle +tactics can exploit logic programming techniques. +