--- a/doc-src/TutorialI/Misc/consts.thy Fri Jan 05 10:19:32 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,5 +0,0 @@
-(*<*)theory "consts" = Main:;
-(*>*)consts nand :: gate
- exor :: gate(*<*)
-end
-(*>*)
--- a/doc-src/TutorialI/Misc/document/natsum.tex Fri Jan 05 10:19:32 2001 +0100
+++ b/doc-src/TutorialI/Misc/document/natsum.tex Fri Jan 05 13:10:37 2001 +0100
@@ -51,7 +51,7 @@
to prove the goal (although 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 an explicit type constraint, for example
- \isa{x\ {\isacharplus}\ {\isadigit{0}}\ {\isacharequal}\ x}. If there is enough contextual information this
+ \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.
\end{warn}
--- a/doc-src/TutorialI/Misc/document/simp.tex Fri Jan 05 10:19:32 2001 +0100
+++ b/doc-src/TutorialI/Misc/document/simp.tex Fri Jan 05 13:10:37 2001 +0100
@@ -140,19 +140,19 @@
enough lemmas that characterize the concept sufficiently for us to forget the
original definition. For example, given%
\end{isamarkuptext}%
-\isacommand{constdefs}\ exor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline
-\ \ \ \ \ \ \ \ \ {\isachardoublequote}exor\ A\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}%
+\isacommand{constdefs}\ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline
+\ \ \ \ \ \ \ \ \ {\isachardoublequote}xor\ A\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}%
\begin{isamarkuptext}%
\noindent
we may want to prove%
\end{isamarkuptext}%
-\isacommand{lemma}\ {\isachardoublequote}exor\ A\ {\isacharparenleft}{\isasymnot}A{\isacharparenright}{\isachardoublequote}%
+\isacommand{lemma}\ {\isachardoublequote}xor\ A\ {\isacharparenleft}{\isasymnot}A{\isacharparenright}{\isachardoublequote}%
\begin{isamarkuptxt}%
\noindent
Typically, the opening move consists in \emph{unfolding} the definition(s), which we need to
get started, but nothing else:\indexbold{*unfold}\indexbold{definition!unfolding}%
\end{isamarkuptxt}%
-\isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}exor{\isacharunderscore}def{\isacharparenright}%
+\isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}xor{\isacharunderscore}def{\isacharparenright}%
\begin{isamarkuptxt}%
\noindent
In this particular case, the resulting goal
@@ -161,7 +161,7 @@
\end{isabelle}
can be proved by simplification. Thus we could have proved the lemma outright by%
\end{isamarkuptxt}%
-\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ exor{\isacharunderscore}def{\isacharparenright}%
+\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ xor{\isacharunderscore}def{\isacharparenright}%
\begin{isamarkuptext}%
\noindent
Of course we can also unfold definitions in the middle of a proof.
--- a/doc-src/TutorialI/Misc/document/types.tex Fri Jan 05 10:19:32 2001 +0100
+++ b/doc-src/TutorialI/Misc/document/types.tex Fri Jan 05 13:10:37 2001 +0100
@@ -12,29 +12,29 @@
type:%
\end{isamarkuptext}%
\isacommand{consts}\ nand\ {\isacharcolon}{\isacharcolon}\ gate\isanewline
-\ \ \ \ \ \ \ exor\ {\isacharcolon}{\isacharcolon}\ gate%
+\ \ \ \ \ \ \ xor\ \ {\isacharcolon}{\isacharcolon}\ gate%
+\isamarkupsubsection{Constant definitions%
+}
+%
\begin{isamarkuptext}%
-\subsection{Constant definitions}
-\label{sec:ConstDefinitions}
-\indexbold{definition}
-
-The above constants \isa{nand} and \isa{exor} are non-recursive and can
+\label{sec:ConstDefinitions}\indexbold{definition}%
+The above constants \isa{nand} and \isa{xor} are non-recursive and can
therefore be defined directly by%
\end{isamarkuptext}%
\isacommand{defs}\ nand{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}nand\ A\ B\ {\isasymequiv}\ {\isasymnot}{\isacharparenleft}A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}\isanewline
-\ \ \ \ \ exor{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}exor\ A\ B\ {\isasymequiv}\ A\ {\isasymand}\ {\isasymnot}B\ {\isasymor}\ {\isasymnot}A\ {\isasymand}\ B{\isachardoublequote}%
+\ \ \ \ \ xor{\isacharunderscore}def{\isacharcolon}\ \ {\isachardoublequote}xor\ A\ B\ \ {\isasymequiv}\ A\ {\isasymand}\ {\isasymnot}B\ {\isasymor}\ {\isasymnot}A\ {\isasymand}\ B{\isachardoublequote}%
\begin{isamarkuptext}%
\noindent%
where \isacommand{defs}\indexbold{*defs} is a keyword and
-\isa{nand{\isacharunderscore}def} and \isa{exor{\isacharunderscore}def} are user-supplied names.
+\isa{nand{\isacharunderscore}def} and \isa{xor{\isacharunderscore}def} are user-supplied names.
The symbol \indexboldpos{\isasymequiv}{$IsaEq} is a special form of equality
that must be used in constant definitions.
Declarations and definitions can also be merged%
\end{isamarkuptext}%
\isacommand{constdefs}\ nor\ {\isacharcolon}{\isacharcolon}\ gate\isanewline
\ \ \ \ \ \ \ \ \ {\isachardoublequote}nor\ A\ B\ {\isasymequiv}\ {\isasymnot}{\isacharparenleft}A\ {\isasymor}\ B{\isacharparenright}{\isachardoublequote}\isanewline
-\ \ \ \ \ \ \ \ \ \ exor{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ gate\isanewline
-\ \ \ \ \ \ \ \ \ {\isachardoublequote}exor{\isadigit{2}}\ A\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymor}\ B{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}{\isasymnot}A\ {\isasymor}\ {\isasymnot}B{\isacharparenright}{\isachardoublequote}%
+\ \ \ \ \ \ \ \ \ \ xor{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ gate\isanewline
+\ \ \ \ \ \ \ \ \ {\isachardoublequote}xor{\isadigit{2}}\ A\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymor}\ B{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}{\isasymnot}A\ {\isasymor}\ {\isasymnot}B{\isacharparenright}{\isachardoublequote}%
\begin{isamarkuptext}%
\noindent\indexbold{*constdefs}%
in which case the default name of each definition is $f$\isa{{\isacharunderscore}def}, where
--- a/doc-src/TutorialI/Misc/natsum.thy Fri Jan 05 10:19:32 2001 +0100
+++ b/doc-src/TutorialI/Misc/natsum.thy Fri Jan 05 13:10:37 2001 +0100
@@ -49,7 +49,7 @@
to prove the goal (although 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 an explicit type constraint, for example
- @{prop"x+0 = (x::nat)"}. If there is enough contextual information this
+ @{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 overloaded.
\end{warn}
--- a/doc-src/TutorialI/Misc/simp.thy Fri Jan 05 10:19:32 2001 +0100
+++ b/doc-src/TutorialI/Misc/simp.thy Fri Jan 05 13:10:37 2001 +0100
@@ -136,28 +136,28 @@
original definition. For example, given
*}
-constdefs exor :: "bool \<Rightarrow> bool \<Rightarrow> bool"
- "exor A B \<equiv> (A \<and> \<not>B) \<or> (\<not>A \<and> B)";
+constdefs xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"
+ "xor A B \<equiv> (A \<and> \<not>B) \<or> (\<not>A \<and> B)";
text{*\noindent
we may want to prove
*}
-lemma "exor A (\<not>A)";
+lemma "xor A (\<not>A)";
txt{*\noindent
Typically, the opening move consists in \emph{unfolding} the definition(s), which we need to
get started, but nothing else:\indexbold{*unfold}\indexbold{definition!unfolding}
*}
-apply(simp only:exor_def);
+apply(simp only:xor_def);
txt{*\noindent
In this particular case, the resulting goal
@{subgoals[display,indent=0]}
can be proved by simplification. Thus we could have proved the lemma outright by
-*}(*<*)oops;lemma "exor A (\<not>A)";(*>*)
-apply(simp add: exor_def)
+*}(*<*)oops;lemma "xor A (\<not>A)";(*>*)
+apply(simp add: xor_def)
(*<*)done(*>*)
text{*\noindent
Of course we can also unfold definitions in the middle of a proof.
--- a/doc-src/TutorialI/Misc/types.thy Fri Jan 05 10:19:32 2001 +0100
+++ b/doc-src/TutorialI/Misc/types.thy Fri Jan 05 13:10:37 2001 +0100
@@ -1,6 +1,5 @@
-(*<*)
-theory "types" = Main:;
-(*>*)types number = nat
+(*<*)theory "types" = Main:(*>*)
+types number = nat
gate = "bool \<Rightarrow> bool \<Rightarrow> bool"
('a,'b)alist = "('a \<times> 'b)list";
@@ -12,23 +11,21 @@
*}
consts nand :: gate
- exor :: gate;
+ xor :: gate;
-text{*
-\subsection{Constant definitions}
-\label{sec:ConstDefinitions}
-\indexbold{definition}
+subsection{*Constant definitions*}
-The above constants @{term"nand"} and @{term"exor"} are non-recursive and can
+text{*\label{sec:ConstDefinitions}\indexbold{definition}%
+The above constants @{term"nand"} and @{term"xor"} are non-recursive and can
therefore be defined directly by
*}
defs nand_def: "nand A B \<equiv> \<not>(A \<and> B)"
- exor_def: "exor A B \<equiv> A \<and> \<not>B \<or> \<not>A \<and> B";
+ xor_def: "xor A B \<equiv> A \<and> \<not>B \<or> \<not>A \<and> B";
text{*\noindent%
where \isacommand{defs}\indexbold{*defs} is a keyword and
-@{thm[source]nand_def} and @{thm[source]exor_def} are user-supplied names.
+@{thm[source]nand_def} and @{thm[source]xor_def} are user-supplied names.
The symbol \indexboldpos{\isasymequiv}{$IsaEq} is a special form of equality
that must be used in constant definitions.
Declarations and definitions can also be merged
@@ -36,11 +33,10 @@
constdefs nor :: gate
"nor A B \<equiv> \<not>(A \<or> B)"
- exor2 :: gate
- "exor2 A B \<equiv> (A \<or> B) \<and> (\<not>A \<or> \<not>B)";
+ xor2 :: gate
+ "xor2 A B \<equiv> (A \<or> B) \<and> (\<not>A \<or> \<not>B)";
text{*\noindent\indexbold{*constdefs}%
in which case the default name of each definition is $f$@{text"_def"}, where
-$f$ is the name of the defined constant.*}(*<*)
-end
-(*>*)
+$f$ is the name of the defined constant.*}
+(*<*)end(*>*)