--- a/doc-src/TutorialI/Documents/Documents.thy Wed Jun 22 07:54:13 2005 +0200
+++ b/doc-src/TutorialI/Documents/Documents.thy Wed Jun 22 09:26:18 2005 +0200
@@ -630,8 +630,8 @@
parsing and type-checking. Document preparation enables symbolic
output by default.
- \medskip The next example includes an option to modify Isabelle's
- \verb,show_types, flag. The antiquotation
+ \medskip The next example includes an option to show the type of all
+ variables. The antiquotation
\texttt{{\at}}\verb,{term [show_types] "%x y. x"}, produces the
output @{term [show_types] "%x y. x"}. Type inference has figured
out the most general typings in the present theory context. Terms
--- a/doc-src/TutorialI/Documents/document/Documents.tex Wed Jun 22 07:54:13 2005 +0200
+++ b/doc-src/TutorialI/Documents/document/Documents.tex Wed Jun 22 09:26:18 2005 +0200
@@ -656,8 +656,8 @@
parsing and type-checking. Document preparation enables symbolic
output by default.
- \medskip The next example includes an option to modify Isabelle's
- \verb,show_types, flag. The antiquotation
+ \medskip The next example includes an option to show the type of all
+ variables. The antiquotation
\texttt{{\at}}\verb,{term [show_types] "%x y. x"}, produces the
output \isa{{\isasymlambda}{\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isacharparenright}\ y{\isasymColon}{\isacharprime}b{\isachardot}\ x}. Type inference has figured
out the most general typings in the present theory context. Terms
--- a/doc-src/TutorialI/Inductive/document/Advanced.tex Wed Jun 22 07:54:13 2005 +0200
+++ b/doc-src/TutorialI/Inductive/document/Advanced.tex Wed Jun 22 09:26:18 2005 +0200
@@ -2,7 +2,7 @@
\begin{isabellebody}%
\def\isabellecontext{Advanced}%
\isanewline
-\isacommand{theory}\ Advanced\ {\isacharequal}\ Even{\isacharcolon}\isanewline
+\isacommand{theory}\ Advanced\ \isakeyword{imports}\ Even\ \isakeyword{begin}\isanewline
\isanewline
\isanewline
\isamarkupfalse%
--- a/doc-src/TutorialI/Inductive/document/Even.tex Wed Jun 22 07:54:13 2005 +0200
+++ b/doc-src/TutorialI/Inductive/document/Even.tex Wed Jun 22 09:26:18 2005 +0200
@@ -2,7 +2,7 @@
\begin{isabellebody}%
\def\isabellecontext{Even}%
\isanewline
-\isacommand{theory}\ Even\ {\isacharequal}\ Main{\isacharcolon}\isanewline
+\isacommand{theory}\ Even\ \isakeyword{imports}\ Main\ \isakeyword{begin}\isanewline
\isanewline
\isanewline
\isamarkupfalse%
--- a/doc-src/TutorialI/Misc/document/natsum.tex Wed Jun 22 07:54:13 2005 +0200
+++ b/doc-src/TutorialI/Misc/document/natsum.tex Wed Jun 22 09:26:18 2005 +0200
@@ -55,7 +55,8 @@
declared. As a consequence, you will be unable to prove the
goal. To alert you to such pitfalls, Isabelle flags numerals without a
fixed type in its output: \isa{x\ {\isacharplus}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharequal}\ x}. (In the absence of a numeral,
- it may take you some time to realize what has happened if \isa{show{\isacharunderscore}types} is not set). In this particular example, you need to include
+ it may take you some time to realize what has happened if \pgmenu{Show
+ Types} is not set). In this particular example, you need to include
an explicit type constraint, for example \isa{x{\isacharplus}{\isadigit{0}}\ {\isacharequal}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}}. If there
is enough contextual information this may not be necessary: \isa{Suc\ x\ {\isacharequal}\ x} automatically implies \isa{x{\isacharcolon}{\isacharcolon}nat} because \isa{Suc} is not
overloaded.
--- a/doc-src/TutorialI/Misc/document/simp.tex Wed Jun 22 07:54:13 2005 +0200
+++ b/doc-src/TutorialI/Misc/document/simp.tex Wed Jun 22 09:26:18 2005 +0200
@@ -441,7 +441,7 @@
\begin{isamarkuptext}%
\indexbold{tracing the simplifier}
Using the simplifier effectively may take a bit of experimentation. Set the
-Proof General flag \textsf{Isabelle} $>$ \textsf{Settings} $>$ \textsf{Trace Simplifier} to get a better idea of what is going on:%
+Proof General flag \pgmenu{Isabelle} $>$ \pgmenu{Settings} $>$ \pgmenu{Trace Simplifier} to get a better idea of what is going on:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\ {\isachardoublequote}rev\ {\isacharbrackleft}a{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isanewline
@@ -451,7 +451,7 @@
%
\begin{isamarkuptext}%
\noindent
-produces the following trace in Proof General's \textsf{Trace} buffer:
+produces the following trace in Proof General's \pgmenu{Trace} buffer:
\begin{ttbox}\makeatother
[1]Applying instance of rewrite rule "List.rev.simps_2":
@@ -491,7 +491,7 @@
Many other hints about the simplifier's actions may appear.
In more complicated cases, the trace can be very lengthy. Thus it is
-advisable to reset the \textsf{Trace Simplifier} flag after having
+advisable to reset the \pgmenu{Trace Simplifier} flag after having
obtained the desired trace.%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -501,12 +501,13 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
+\indexbold{finding theorems}\indexbold{searching theorems}
Isabelle's large database of already proved theorems requires
and offers a powerful yet simple search engine. Its only limitation is
its restriction to the theories currently loaded.
\begin{pgnote}
-The search engine is started by clicking on Proof General's \textsf{Find} icon.
+The search engine is started by clicking on Proof General's \pgmenu{Find} icon.
You specify your search textually in the input buffer at the bottom
of the window.
\end{pgnote}
@@ -543,13 +544,14 @@
\begin{ttbox}
simp: "_ * (_ + _)"
\end{ttbox}
-This searches all (possibly conditional) equations of the form
+This searches \emph{all} (possibly conditional) equations of the form
\begin{isabelle}%
\ \ \ \ \ {\isacharunderscore}\ {\isacharasterisk}\ {\isacharparenleft}{\isacharunderscore}\ {\isacharplus}\ {\isacharunderscore}{\isacharparenright}\ {\isacharequal}\ {\isasymdots}%
\end{isabelle}
-i.e.\ all distributivity rules.
+not just those with a \isa{simp} attribute.
Note that the given pattern needs to be simplified
-at the root, not somewhere inside.
+at the root, not somewhere inside: for example, commutativity of \isa{{\isacharplus}}
+does not match.
You may also search theorems by name. To make this useful you merely
need to give a substring. For example, you could try and search for all
@@ -561,9 +563,10 @@
Search criteria can also be negated by prefixing them with ``\texttt{-}'':
\begin{ttbox}
--name: HOL
+-name: List
\end{ttbox}
-finds theorems whose name does not contain \texttt{HOL}. This is useful for
+finds theorems whose name does not contain \texttt{List}. This can be useful,
+for example, for
excluding particular theories from the search because the (long) name of
a theorem contains the name of the theory it comes from.
@@ -571,10 +574,17 @@
\begin{ttbox}
"_ + _" -"_ - _" -simp: "_ * (_ + _)" name: assoc
\end{ttbox}
-looks for theorems containg a plus but no minus which are not distributivity
-rules and whose name contains \texttt{assoc}.
+looks for theorems containg a plus but no minus which do not simplify
+\mbox{\isa{{\isacharunderscore}\ {\isacharasterisk}\ {\isacharparenleft}{\isacharunderscore}\ {\isacharplus}\ {\isacharunderscore}{\isacharparenright}}} at the root and whose name contains \texttt{assoc}.
+
+Further search criteria are explained in \S\ref{sec:find:ied}.
-Further search criteria are explained in \S\ref{sec:Find:ied}.%
+\begin{pgnote}
+Proof General keeps a history of all your search expressions.
+If you click on \pgmenu{Find}, you can use the arrow keys to scroll
+through previous searches and just modify them. This saves you having
+to type in lengthy expressions again and again.
+\end{pgnote}%
\end{isamarkuptext}%
\isamarkuptrue%
\isamarkupfalse%
--- a/doc-src/TutorialI/Misc/natsum.thy Wed Jun 22 07:54:13 2005 +0200
+++ b/doc-src/TutorialI/Misc/natsum.thy Wed Jun 22 09:26:18 2005 +0200
@@ -1,5 +1,5 @@
(*<*)
-theory natsum imports Main begin;
+theory natsum imports Main begin
(*>*)
text{*\noindent
In particular, there are @{text"case"}-expressions, for example
@@ -7,17 +7,17 @@
primitive recursion, for example
*}
-consts sum :: "nat \<Rightarrow> nat";
+consts sum :: "nat \<Rightarrow> nat"
primrec "sum 0 = 0"
- "sum (Suc n) = Suc n + sum n";
+ "sum (Suc n) = Suc n + sum n"
text{*\noindent
and induction, for example
*}
-lemma "sum n + sum n = n*(Suc n)";
-apply(induct_tac n);
-apply(auto);
+lemma "sum n + sum n = n*(Suc n)"
+apply(induct_tac n)
+apply(auto)
done
text{*\newcommand{\mystar}{*%
@@ -44,8 +44,8 @@
declared. As a consequence, you will be unable to prove the
goal. To alert you to such pitfalls, Isabelle flags numerals without a
fixed type in its output: @{prop"x+0 = x"}. (In the absence of a numeral,
- it may take you some time to realize what has happened if @{text
- show_types} is not set). In this particular example, you need to include
+ it may take you some time to realize what has happened if \pgmenu{Show
+ Types} is not set). In this particular example, you need to include
an explicit type constraint, for example @{text"x+0 = (x::nat)"}. If there
is enough contextual information this may not be necessary: @{prop"Suc x =
x"} automatically implies @{text"x::nat"} because @{term Suc} is not
@@ -95,7 +95,7 @@
@{text"\<le>"} and @{text"<"}, and the operations @{text"+"}, @{text"-"},
@{term min} and @{term max}. For example, *}
-lemma "min i (max j (k*k)) = max (min (k*k) i) (min i (j::nat))";
+lemma "min i (max j (k*k)) = max (min (k*k) i) (min i (j::nat))"
apply(arith)
(*<*)done(*>*)
--- a/doc-src/TutorialI/Misc/simp.thy Wed Jun 22 07:54:13 2005 +0200
+++ b/doc-src/TutorialI/Misc/simp.thy Wed Jun 22 09:26:18 2005 +0200
@@ -367,7 +367,7 @@
subsection{*Tracing*}
text{*\indexbold{tracing the simplifier}
Using the simplifier effectively may take a bit of experimentation. Set the
-Proof General flag \textsf{Isabelle} $>$ \textsf{Settings} $>$ \textsf{Trace Simplifier} to get a better idea of what is going on:
+Proof General flag \pgmenu{Isabelle} $>$ \pgmenu{Settings} $>$ \pgmenu{Trace Simplifier} to get a better idea of what is going on:
*}
lemma "rev [a] = []"
@@ -375,7 +375,7 @@
(*<*)oops(*>*)
text{*\noindent
-produces the following trace in Proof General's \textsf{Trace} buffer:
+produces the following trace in Proof General's \pgmenu{Trace} buffer:
\begin{ttbox}\makeatother
[1]Applying instance of rewrite rule "List.rev.simps_2":
@@ -415,17 +415,18 @@
Many other hints about the simplifier's actions may appear.
In more complicated cases, the trace can be very lengthy. Thus it is
-advisable to reset the \textsf{Trace Simplifier} flag after having
+advisable to reset the \pgmenu{Trace Simplifier} flag after having
obtained the desired trace. *}
subsection{*Finding Theorems*}
-text{* Isabelle's large database of already proved theorems requires
+text{*\indexbold{finding theorems}\indexbold{searching theorems}
+Isabelle's large database of already proved theorems requires
and offers a powerful yet simple search engine. Its only limitation is
its restriction to the theories currently loaded.
\begin{pgnote}
-The search engine is started by clicking on Proof General's \textsf{Find} icon.
+The search engine is started by clicking on Proof General's \pgmenu{Find} icon.
You specify your search textually in the input buffer at the bottom
of the window.
\end{pgnote}
@@ -462,11 +463,12 @@
\begin{ttbox}
simp: "_ * (_ + _)"
\end{ttbox}
-This searches all (possibly conditional) equations of the form
+This searches \emph{all} (possibly conditional) equations of the form
@{text[display]"_ * (_ + _) = \<dots>"}
-i.e.\ all distributivity rules.
+not just those with a \isa{simp} attribute.
Note that the given pattern needs to be simplified
-at the root, not somewhere inside.
+at the root, not somewhere inside: for example, commutativity of @{text"+"}
+does not match.
You may also search theorems by name. To make this useful you merely
need to give a substring. For example, you could try and search for all
@@ -478,9 +480,10 @@
Search criteria can also be negated by prefixing them with ``\texttt{-}'':
\begin{ttbox}
--name: HOL
+-name: List
\end{ttbox}
-finds theorems whose name does not contain \texttt{HOL}. This is useful for
+finds theorems whose name does not contain \texttt{List}. This can be useful,
+for example, for
excluding particular theories from the search because the (long) name of
a theorem contains the name of the theory it comes from.
@@ -488,12 +491,18 @@
\begin{ttbox}
"_ + _" -"_ - _" -simp: "_ * (_ + _)" name: assoc
\end{ttbox}
-looks for theorems containg a plus but no minus which are not distributivity
-rules and whose name contains \texttt{assoc}.
+looks for theorems containg a plus but no minus which do not simplify
+\mbox{@{text"_ * (_ + _)"}} at the root and whose name contains \texttt{assoc}.
Further search criteria are explained in \S\ref{sec:find:ied}.
+
+\begin{pgnote}
+Proof General keeps a history of all your search expressions.
+If you click on \pgmenu{Find}, you can use the arrow keys to scroll
+through previous searches and just modify them. This saves you having
+to type in lengthy expressions again and again.
+\end{pgnote}
*}
-
(*<*)
end
(*>*)
--- a/doc-src/TutorialI/Rules/rules.tex Wed Jun 22 07:54:13 2005 +0200
+++ b/doc-src/TutorialI/Rules/rules.tex Wed Jun 22 09:26:18 2005 +0200
@@ -635,10 +635,10 @@
filled in later, sometimes in stages and often automatically.
\begin{pgnote}
-If unification fails when you think it should succeed, try setting the Proof General flag \textsf{Isabelle} $>$ \textsf{Settings} $>$
-\textsf{Trace Unification},
+If unification fails when you think it should succeed, try setting the Proof General flag \pgmenu{Isabelle} $>$ \pgmenu{Settings} $>$
+\pgmenu{Trace Unification},
which makes Isabelle show the cause of unification failures (in Proof
-General's \textsf{Trace} buffer).
+General's \pgmenu{Trace} buffer).
\end{pgnote}
\noindent
For example, suppose we are trying to prove this subgoal by assumption:
--- a/doc-src/TutorialI/Types/document/Numbers.tex Wed Jun 22 07:54:13 2005 +0200
+++ b/doc-src/TutorialI/Types/document/Numbers.tex Wed Jun 22 09:26:18 2005 +0200
@@ -2,7 +2,7 @@
\begin{isabellebody}%
\def\isabellecontext{Numbers}%
\isanewline
-\isacommand{theory}\ Numbers\ {\isacharequal}\ Real{\isacharcolon}\isanewline
+\isacommand{theory}\ Numbers\ \isakeyword{imports}\ Real\ \isakeyword{begin}\isanewline
\isanewline
\isamarkupfalse%
\isacommand{ML}\ {\isachardoublequote}Pretty{\isachardot}setmargin\ {\isadigit{6}}{\isadigit{4}}{\isachardoublequote}\isanewline
--- a/doc-src/TutorialI/Types/numerics.tex Wed Jun 22 07:54:13 2005 +0200
+++ b/doc-src/TutorialI/Types/numerics.tex Wed Jun 22 09:26:18 2005 +0200
@@ -344,8 +344,8 @@
Type \isa{real} is only available in the logic HOL-Complex, which is
HOL extended with a definitional development of the real and complex
numbers. Base your theory upon theory \thydx{Complex_Main}, not the
-usual \isa{Main}, and set the Proof General menu item \textsf{Isabelle} $>$
-\textsf{Logics} $>$ \textsf{HOL-Complex}.%
+usual \isa{Main}, and set the Proof General menu item \pgmenu{Isabelle} $>$
+\pgmenu{Logics} $>$ \pgmenu{HOL-Complex}.%
\index{real numbers|)}\index{*real (type)|)}
\end{warn}
@@ -400,8 +400,8 @@
Theorems \isa{field_mult_eq_0_iff} and \isa{field_mult_cancel_right}
express the same properties, only for fields.
\begin{pgnote}
-Setting the flag \textsf{Isabelle} $>$ \textsf{Settings} $>$
-\textsf{Show Sorts} will display the type classes of all type variables.
+Setting the flag \pgmenu{Isabelle} $>$ \pgmenu{Settings} $>$
+\pgmenu{Show Sorts} will display the type classes of all type variables.
\end{pgnote}
\noindent
Here is how the theorem \isa{field_mult_cancel_right} appears with the flag set.
--- a/doc-src/TutorialI/basics.tex Wed Jun 22 07:54:13 2005 +0200
+++ b/doc-src/TutorialI/basics.tex Wed Jun 22 09:26:18 2005 +0200
@@ -142,8 +142,8 @@
and keeps quiet about it. Occasionally this may lead to
misunderstandings between you and the system. If anything strange
happens, we recommend that you ask Isabelle to display all type
- information via the Proof General menu item \textsf{Isabelle} $>$
- \textsf{Settings} $>$ \textsf{Show Types} (see \S\ref{sec:interface}
+ information via the Proof General menu item \pgmenu{Isabelle} $>$
+ \pgmenu{Settings} $>$ \pgmenu{Show Types} (see \S\ref{sec:interface}
for details).
\end{warn}%
\index{types|)}
@@ -264,8 +264,8 @@
Isabelle echoes your input, you can see which parentheses are dropped
--- they were superfluous. If you are unsure how to interpret
Isabelle's output because you don't know where the (dropped)
-parentheses go, set the Proof General flag \textsf{Isabelle} $>$
-\textsf{Settings} $>$ \textsf{Show Brackets} (see \S\ref{sec:interface}).
+parentheses go, set the Proof General flag \pgmenu{Isabelle} $>$
+\pgmenu{Settings} $>$ \pgmenu{Show Brackets} (see \S\ref{sec:interface}).
\end{warn}
@@ -309,7 +309,7 @@
should be avoided. Most of the tutorial is independent of the
interface and is phrased in a neutral language. For example, the
phrase ``to abandon a proof'' corresponds to the obvious
-action of clicking on the \textsf{Undo} symbol in Proof General.
+action of clicking on the \pgmenu{Undo} symbol in Proof General.
Proof General specific information is often displayed in paragraphs
identified by a miniature Proof General icon. Here are two examples:
\begin{pgnote}
@@ -320,15 +320,15 @@
in the appendix.
Note that by default x-symbols are not enabled. You have to switch
-them on via the menu item \textsf{Proof-General} $>$ \textsf{Options} $>$
-\textsf{X-Symbols} (and save the option via the top-level
-\textsf{Options} menu).
+them on via the menu item \pgmenu{Proof-General} $>$ \pgmenu{Options} $>$
+\pgmenu{X-Symbols} (and save the option via the top-level
+\pgmenu{Options} menu).
\end{pgnote}
\begin{pgnote}
-Proof General offers the \textsf{Isabelle} menu for displaying
+Proof General offers the \pgmenu{Isabelle} menu for displaying
information and setting flags. A particularly useful flag is
-\textsf{Isabelle} $>$ \textsf{Settings} $>$ \textsf{Show Types} which
+\pgmenu{Isabelle} $>$ \pgmenu{Settings} $>$ \pgdx{Show Types} which
causes Isabelle to output the type information that is usually
suppressed. This is indispensible in case of errors of all kinds
because often the types reveal the source of the problem. Once you
@@ -345,10 +345,7 @@
for more details.}.
\begin{pgnote}
-You can choose a different logic via the \textsf{Isabelle} $>$
-\textsf{Logics} menu. For example, you may want to work in the real
+You can choose a different logic via the \pgmenu{Isabelle} $>$
+\pgmenu{Logics} menu. For example, you may want to work in the real
numbers, an extension of HOL (see \S\ref{sec:real}).
-% This is just excess baggage:
-%(You have to restart Proof General if you only compile the new logic
-%after having launching Proof General already).
\end{pgnote}
--- a/doc-src/TutorialI/fp.tex Wed Jun 22 07:54:13 2005 +0200
+++ b/doc-src/TutorialI/fp.tex Wed Jun 22 09:26:18 2005 +0200
@@ -106,7 +106,7 @@
Manual~\cite{isabelle-isar-ref}.
\begin{pgnote}
-Clicking on the \textsf{State} button redisplays the current proof state.
+Clicking on the \pgmenu{State} button redisplays the current proof state.
This is helpful in case commands like \isacommand{thm} have overwritten it.
\end{pgnote}
--- a/doc-src/TutorialI/tutorial.sty Wed Jun 22 07:54:13 2005 +0200
+++ b/doc-src/TutorialI/tutorial.sty Wed Jun 22 09:26:18 2005 +0200
@@ -44,6 +44,7 @@
\newcommand\methdx[1]{\isa{#1}\index{#1@\protect\isa{#1} (method)}}
\newcommand\tooldx[1]{\isa{#1}\index{#1@\protect\isa{#1} (tool)}}
\newcommand\settdx[1]{\isa{#1}\index{#1@\protect\isa{#1} (setting)}}
+\newcommand\pgdx[1]{\pgmenu{#1}\index{#1@\protect\pgmenu{#1} (Proof General)}}
%set argument in \bf font and index in ROMAN font (for definitions in text!)
\newcommand\bfindex[1]{{\bf#1}\index{#1|bold}\@}
@@ -123,7 +124,7 @@
\small \noindent \hangindent\parindent \hangafter=-2
\hbox to0pt{\hskip-\hangindent \pghead\hfill}\ignorespaces}%
{\par\endgroup\medbreak}
-
+\newcommand{\pgmenu}[1]{\textsf{#1}}
%%%% Standard logical symbols