--- a/doc-src/IsarRef/Thy/Spec.thy Sun Apr 15 13:15:14 2012 +0200
+++ b/doc-src/IsarRef/Thy/Spec.thy Sun Apr 15 13:21:13 2012 +0200
@@ -104,8 +104,14 @@
section {* Local theory targets \label{sec:target} *}
-text {* A local theory target is a context managed separately within
- the enclosing theory. Contexts may introduce parameters (fixed
+text {*
+ \begin{matharray}{rcll}
+ @{command_def "context"} & : & @{text "theory \<rightarrow> local_theory"} \\
+ @{command_def (local) "end"} & : & @{text "local_theory \<rightarrow> theory"} \\
+ \end{matharray}
+
+ A local theory target is a context managed separately within the
+ enclosing theory. Contexts may introduce parameters (fixed
variables) and assumptions (hypotheses). Definitions and theorems
depending on the context may be added incrementally later on.
@@ -119,11 +125,6 @@
targets, like @{command "locale"}, @{command "class"}, @{command
"instantiation"}, @{command "overloading"}.
- \begin{matharray}{rcll}
- @{command_def "context"} & : & @{text "theory \<rightarrow> local_theory"} \\
- @{command_def (local) "end"} & : & @{text "local_theory \<rightarrow> theory"} \\
- \end{matharray}
-
@{rail "
@@{command context} (@{syntax nameref} | (@{syntax context_elem}+)) @'begin'
;
@@ -275,6 +276,12 @@
section {* Generic declarations *}
text {*
+ \begin{matharray}{rcl}
+ @{command_def "declaration"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
+ @{command_def "syntax_declaration"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
+ @{command_def "declare"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
+ \end{matharray}
+
Arbitrary operations on the background context may be wrapped-up as
generic declaration elements. Since the underlying concept of local
theories may be subject to later re-interpretation, there is an
@@ -284,12 +291,6 @@
case: it consists of a theorem which is applied to the context by
means of an attribute.
- \begin{matharray}{rcl}
- @{command_def "declaration"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
- @{command_def "syntax_declaration"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
- @{command_def "declare"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
- \end{matharray}
-
@{rail "
(@@{command declaration} | @@{command syntax_declaration})
('(' @'pervasive' ')')? \\ @{syntax target}? @{syntax text}
@@ -516,13 +517,6 @@
subsection {* Locale interpretations *}
text {*
- Locale expressions may be instantiated, and the instantiated facts
- added to the current context. This requires a proof of the
- instantiated specification and is called \emph{locale
- interpretation}. Interpretation is possible in locales @{command
- "sublocale"}, theories (command @{command "interpretation"}) and
- also within a proof body (command @{command "interpret"}).
-
\begin{matharray}{rcl}
@{command_def "interpretation"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
@{command_def "interpret"} & : & @{text "proof(state) | proof(chain) \<rightarrow> proof(prove)"} \\
@@ -531,6 +525,13 @@
@{command_def "print_interps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
\end{matharray}
+ Locale expressions may be instantiated, and the instantiated facts
+ added to the current context. This requires a proof of the
+ instantiated specification and is called \emph{locale
+ interpretation}. Interpretation is possible in locales @{command
+ "sublocale"}, theories (command @{command "interpretation"}) and
+ also within a proof body (command @{command "interpret"}).
+
@{rail "
@@{command interpretation} @{syntax locale_expr} equations?
;
@@ -652,15 +653,6 @@
section {* Classes \label{sec:class} *}
text {*
- A class is a particular locale with \emph{exactly one} type variable
- @{text \<alpha>}. Beyond the underlying locale, a corresponding type class
- is established which is interpreted logically as axiomatic type
- class \cite{Wenzel:1997:TPHOL} whose logical content are the
- assumptions of the locale. Thus, classes provide the full
- generality of locales combined with the commodity of type classes
- (notably type-inference). See \cite{isabelle-classes} for a short
- tutorial.
-
\begin{matharray}{rcl}
@{command_def "class"} & : & @{text "theory \<rightarrow> local_theory"} \\
@{command_def "instantiation"} & : & @{text "theory \<rightarrow> local_theory"} \\
@@ -672,6 +664,15 @@
@{method_def intro_classes} & : & @{text method} \\
\end{matharray}
+ A class is a particular locale with \emph{exactly one} type variable
+ @{text \<alpha>}. Beyond the underlying locale, a corresponding type class
+ is established which is interpreted logically as axiomatic type
+ class \cite{Wenzel:1997:TPHOL} whose logical content are the
+ assumptions of the locale. Thus, classes provide the full
+ generality of locales combined with the commodity of type classes
+ (notably type-inference). See \cite{isabelle-classes} for a short
+ tutorial.
+
@{rail "
@@{command class} class_spec @'begin'?
;
@@ -828,6 +829,10 @@
section {* Unrestricted overloading *}
text {*
+ \begin{matharray}{rcl}
+ @{command_def "overloading"} & : & @{text "theory \<rightarrow> local_theory"} \\
+ \end{matharray}
+
Isabelle/Pure's definitional schemes support certain forms of
overloading (see \secref{sec:consts}). Overloading means that a
constant being declared as @{text "c :: \<alpha> decl"} may be
@@ -840,10 +845,6 @@
The @{command "overloading"} target provides a convenient view for
end-users.
- \begin{matharray}{rcl}
- @{command_def "overloading"} & : & @{text "theory \<rightarrow> local_theory"} \\
- \end{matharray}
-
@{rail "
@@{command overloading} ( spec + ) @'begin'
;
@@ -1059,6 +1060,11 @@
subsection {* Constants and definitions \label{sec:consts} *}
text {*
+ \begin{matharray}{rcl}
+ @{command_def "consts"} & : & @{text "theory \<rightarrow> theory"} \\
+ @{command_def "defs"} & : & @{text "theory \<rightarrow> theory"} \\
+ \end{matharray}
+
Definitions essentially express abbreviations within the logic. The
simplest form of a definition is @{text "c :: \<sigma> \<equiv> t"}, where @{text
c} is a newly declared constant. Isabelle also allows derived forms
@@ -1096,11 +1102,6 @@
corresponding occurrences on some right-hand side need to be an
instance of this, general @{text "d :: \<alpha> \<times> \<beta>"} will be disallowed.
- \begin{matharray}{rcl}
- @{command_def "consts"} & : & @{text "theory \<rightarrow> theory"} \\
- @{command_def "defs"} & : & @{text "theory \<rightarrow> theory"} \\
- \end{matharray}
-
@{rail "
@@{command consts} ((@{syntax name} '::' @{syntax type} @{syntax mixfix}?) +)
;
@@ -1176,10 +1177,15 @@
section {* Oracles *}
-text {* Oracles allow Isabelle to take advantage of external reasoners
- such as arithmetic decision procedures, model checkers, fast
- tautology checkers or computer algebra systems. Invoked as an
- oracle, an external reasoner can create arbitrary Isabelle theorems.
+text {*
+ \begin{matharray}{rcll}
+ @{command_def "oracle"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\
+ \end{matharray}
+
+ Oracles allow Isabelle to take advantage of external reasoners such
+ as arithmetic decision procedures, model checkers, fast tautology
+ checkers or computer algebra systems. Invoked as an oracle, an
+ external reasoner can create arbitrary Isabelle theorems.
It is the responsibility of the user to ensure that the external
reasoner is as trustworthy as the application requires. Another
@@ -1191,10 +1197,6 @@
asserted, and records within the internal derivation object how
presumed theorems depend on unproven suppositions.
- \begin{matharray}{rcll}
- @{command_def "oracle"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\
- \end{matharray}
-
@{rail "
@@{command oracle} @{syntax name} '=' @{syntax text}
"}
--- a/doc-src/IsarRef/Thy/document/Spec.tex Sun Apr 15 13:15:14 2012 +0200
+++ b/doc-src/IsarRef/Thy/document/Spec.tex Sun Apr 15 13:21:13 2012 +0200
@@ -167,8 +167,13 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-A local theory target is a context managed separately within
- the enclosing theory. Contexts may introduce parameters (fixed
+\begin{matharray}{rcll}
+ \indexdef{}{command}{context}\hypertarget{command.context}{\hyperlink{command.context}{\mbox{\isa{\isacommand{context}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
+ \indexdef{local}{command}{end}\hypertarget{command.local.end}{\hyperlink{command.local.end}{\mbox{\isa{\isacommand{end}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
+ \end{matharray}
+
+ A local theory target is a context managed separately within the
+ enclosing theory. Contexts may introduce parameters (fixed
variables) and assumptions (hypotheses). Definitions and theorems
depending on the context may be added incrementally later on.
@@ -181,11 +186,6 @@
accordingly. Such auxiliary contexts may be nested within other
targets, like \hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}}, \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}}, \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}, \hyperlink{command.overloading}{\mbox{\isa{\isacommand{overloading}}}}.
- \begin{matharray}{rcll}
- \indexdef{}{command}{context}\hypertarget{command.context}{\hyperlink{command.context}{\mbox{\isa{\isacommand{context}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
- \indexdef{local}{command}{end}\hypertarget{command.local.end}{\hyperlink{command.local.end}{\mbox{\isa{\isacommand{end}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
- \end{matharray}
-
\begin{railoutput}
\rail@begin{3}{}
\rail@term{\hyperlink{command.context}{\mbox{\isa{\isacommand{context}}}}}[]
@@ -427,7 +427,13 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Arbitrary operations on the background context may be wrapped-up as
+\begin{matharray}{rcl}
+ \indexdef{}{command}{declaration}\hypertarget{command.declaration}{\hyperlink{command.declaration}{\mbox{\isa{\isacommand{declaration}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
+ \indexdef{}{command}{syntax\_declaration}\hypertarget{command.syntax-declaration}{\hyperlink{command.syntax-declaration}{\mbox{\isa{\isacommand{syntax{\isaliteral{5F}{\isacharunderscore}}declaration}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
+ \indexdef{}{command}{declare}\hypertarget{command.declare}{\hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
+ \end{matharray}
+
+ Arbitrary operations on the background context may be wrapped-up as
generic declaration elements. Since the underlying concept of local
theories may be subject to later re-interpretation, there is an
additional dependency on a morphism that tells the difference of the
@@ -436,12 +442,6 @@
case: it consists of a theorem which is applied to the context by
means of an attribute.
- \begin{matharray}{rcl}
- \indexdef{}{command}{declaration}\hypertarget{command.declaration}{\hyperlink{command.declaration}{\mbox{\isa{\isacommand{declaration}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
- \indexdef{}{command}{syntax\_declaration}\hypertarget{command.syntax-declaration}{\hyperlink{command.syntax-declaration}{\mbox{\isa{\isacommand{syntax{\isaliteral{5F}{\isacharunderscore}}declaration}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
- \indexdef{}{command}{declare}\hypertarget{command.declare}{\hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
- \end{matharray}
-
\begin{railoutput}
\rail@begin{5}{}
\rail@bar
@@ -829,13 +829,7 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Locale expressions may be instantiated, and the instantiated facts
- added to the current context. This requires a proof of the
- instantiated specification and is called \emph{locale
- interpretation}. Interpretation is possible in locales \hyperlink{command.sublocale}{\mbox{\isa{\isacommand{sublocale}}}}, theories (command \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}) and
- also within a proof body (command \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}).
-
- \begin{matharray}{rcl}
+\begin{matharray}{rcl}
\indexdef{}{command}{interpretation}\hypertarget{command.interpretation}{\hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
\indexdef{}{command}{interpret}\hypertarget{command.interpret}{\hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{7C}{\isacharbar}}\ proof{\isaliteral{28}{\isacharparenleft}}chain{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
\indexdef{}{command}{sublocale}\hypertarget{command.sublocale}{\hyperlink{command.sublocale}{\mbox{\isa{\isacommand{sublocale}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
@@ -843,6 +837,12 @@
\indexdef{}{command}{print\_interps}\hypertarget{command.print-interps}{\hyperlink{command.print-interps}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}interps}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
\end{matharray}
+ Locale expressions may be instantiated, and the instantiated facts
+ added to the current context. This requires a proof of the
+ instantiated specification and is called \emph{locale
+ interpretation}. Interpretation is possible in locales \hyperlink{command.sublocale}{\mbox{\isa{\isacommand{sublocale}}}}, theories (command \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}) and
+ also within a proof body (command \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}).
+
\begin{railoutput}
\rail@begin{2}{}
\rail@term{\hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}}[]
@@ -1006,16 +1006,7 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-A class is a particular locale with \emph{exactly one} type variable
- \isa{{\isaliteral{5C3C616C7068613E}{\isasymalpha}}}. Beyond the underlying locale, a corresponding type class
- is established which is interpreted logically as axiomatic type
- class \cite{Wenzel:1997:TPHOL} whose logical content are the
- assumptions of the locale. Thus, classes provide the full
- generality of locales combined with the commodity of type classes
- (notably type-inference). See \cite{isabelle-classes} for a short
- tutorial.
-
- \begin{matharray}{rcl}
+\begin{matharray}{rcl}
\indexdef{}{command}{class}\hypertarget{command.class}{\hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
\indexdef{}{command}{instantiation}\hypertarget{command.instantiation}{\hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
\indexdef{}{command}{instance}\hypertarget{command.instance}{\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
@@ -1026,6 +1017,15 @@
\indexdef{}{method}{intro\_classes}\hypertarget{method.intro-classes}{\hyperlink{method.intro-classes}{\mbox{\isa{intro{\isaliteral{5F}{\isacharunderscore}}classes}}}} & : & \isa{method} \\
\end{matharray}
+ A class is a particular locale with \emph{exactly one} type variable
+ \isa{{\isaliteral{5C3C616C7068613E}{\isasymalpha}}}. Beyond the underlying locale, a corresponding type class
+ is established which is interpreted logically as axiomatic type
+ class \cite{Wenzel:1997:TPHOL} whose logical content are the
+ assumptions of the locale. Thus, classes provide the full
+ generality of locales combined with the commodity of type classes
+ (notably type-inference). See \cite{isabelle-classes} for a short
+ tutorial.
+
\begin{railoutput}
\rail@begin{2}{}
\rail@term{\hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}}}[]
@@ -1236,7 +1236,11 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Isabelle/Pure's definitional schemes support certain forms of
+\begin{matharray}{rcl}
+ \indexdef{}{command}{overloading}\hypertarget{command.overloading}{\hyperlink{command.overloading}{\mbox{\isa{\isacommand{overloading}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
+ \end{matharray}
+
+ Isabelle/Pure's definitional schemes support certain forms of
overloading (see \secref{sec:consts}). Overloading means that a
constant being declared as \isa{{\isaliteral{22}{\isachardoublequote}}c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ decl{\isaliteral{22}{\isachardoublequote}}} may be
defined separately on type instances
@@ -1248,10 +1252,6 @@
The \hyperlink{command.overloading}{\mbox{\isa{\isacommand{overloading}}}} target provides a convenient view for
end-users.
- \begin{matharray}{rcl}
- \indexdef{}{command}{overloading}\hypertarget{command.overloading}{\hyperlink{command.overloading}{\mbox{\isa{\isacommand{overloading}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
- \end{matharray}
-
\begin{railoutput}
\rail@begin{2}{}
\rail@term{\hyperlink{command.overloading}{\mbox{\isa{\isacommand{overloading}}}}}[]
@@ -1575,7 +1575,12 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Definitions essentially express abbreviations within the logic. The
+\begin{matharray}{rcl}
+ \indexdef{}{command}{consts}\hypertarget{command.consts}{\hyperlink{command.consts}{\mbox{\isa{\isacommand{consts}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
+ \indexdef{}{command}{defs}\hypertarget{command.defs}{\hyperlink{command.defs}{\mbox{\isa{\isacommand{defs}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
+ \end{matharray}
+
+ Definitions essentially express abbreviations within the logic. The
simplest form of a definition is \isa{{\isaliteral{22}{\isachardoublequote}}c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t{\isaliteral{22}{\isachardoublequote}}}, where \isa{c} is a newly declared constant. Isabelle also allows derived forms
where the arguments of \isa{c} appear on the left, abbreviating a
prefix of \isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}}-abstractions, e.g.\ \isa{{\isaliteral{22}{\isachardoublequote}}c\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x\ y{\isaliteral{2E}{\isachardot}}\ t{\isaliteral{22}{\isachardoublequote}}} may be
@@ -1610,11 +1615,6 @@
corresponding occurrences on some right-hand side need to be an
instance of this, general \isa{{\isaliteral{22}{\isachardoublequote}}d\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{5C3C626574613E}{\isasymbeta}}{\isaliteral{22}{\isachardoublequote}}} will be disallowed.
- \begin{matharray}{rcl}
- \indexdef{}{command}{consts}\hypertarget{command.consts}{\hyperlink{command.consts}{\mbox{\isa{\isacommand{consts}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
- \indexdef{}{command}{defs}\hypertarget{command.defs}{\hyperlink{command.defs}{\mbox{\isa{\isacommand{defs}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
- \end{matharray}
-
\begin{railoutput}
\rail@begin{3}{}
\rail@term{\hyperlink{command.consts}{\mbox{\isa{\isacommand{consts}}}}}[]
@@ -1760,10 +1760,14 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Oracles allow Isabelle to take advantage of external reasoners
- such as arithmetic decision procedures, model checkers, fast
- tautology checkers or computer algebra systems. Invoked as an
- oracle, an external reasoner can create arbitrary Isabelle theorems.
+\begin{matharray}{rcll}
+ \indexdef{}{command}{oracle}\hypertarget{command.oracle}{\hyperlink{command.oracle}{\mbox{\isa{\isacommand{oracle}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} & (axiomatic!) \\
+ \end{matharray}
+
+ Oracles allow Isabelle to take advantage of external reasoners such
+ as arithmetic decision procedures, model checkers, fast tautology
+ checkers or computer algebra systems. Invoked as an oracle, an
+ external reasoner can create arbitrary Isabelle theorems.
It is the responsibility of the user to ensure that the external
reasoner is as trustworthy as the application requires. Another
@@ -1775,10 +1779,6 @@
asserted, and records within the internal derivation object how
presumed theorems depend on unproven suppositions.
- \begin{matharray}{rcll}
- \indexdef{}{command}{oracle}\hypertarget{command.oracle}{\hyperlink{command.oracle}{\mbox{\isa{\isacommand{oracle}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} & (axiomatic!) \\
- \end{matharray}
-
\begin{railoutput}
\rail@begin{1}{}
\rail@term{\hyperlink{command.oracle}{\mbox{\isa{\isacommand{oracle}}}}}[]