# HG changeset patch # User wenzelm # Date 1334488873 -7200 # Node ID 3f704717a67f1dd068959f5e89873a4b02cbbfe6 # Parent a83b25e5bad317ce930803add53b0b321cc33d16 more uniform outline; diff -r a83b25e5bad3 -r 3f704717a67f doc-src/IsarRef/Thy/Spec.thy --- 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 \ local_theory"} \\ + @{command_def (local) "end"} & : & @{text "local_theory \ 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 \ local_theory"} \\ - @{command_def (local) "end"} & : & @{text "local_theory \ 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 \ local_theory"} \\ + @{command_def "syntax_declaration"} & : & @{text "local_theory \ local_theory"} \\ + @{command_def "declare"} & : & @{text "local_theory \ 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 \ local_theory"} \\ - @{command_def "syntax_declaration"} & : & @{text "local_theory \ local_theory"} \\ - @{command_def "declare"} & : & @{text "local_theory \ 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 \ proof(prove)"} \\ @{command_def "interpret"} & : & @{text "proof(state) | proof(chain) \ proof(prove)"} \\ @@ -531,6 +525,13 @@ @{command_def "print_interps"}@{text "\<^sup>*"} & : & @{text "context \"} \\ \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 \}. 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 \ local_theory"} \\ @{command_def "instantiation"} & : & @{text "theory \ 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 \}. 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 \ 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 :: \ 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 \ 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 \ theory"} \\ + @{command_def "defs"} & : & @{text "theory \ theory"} \\ + \end{matharray} + Definitions essentially express abbreviations within the logic. The simplest form of a definition is @{text "c :: \ \ 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 :: \ \ \"} will be disallowed. - \begin{matharray}{rcl} - @{command_def "consts"} & : & @{text "theory \ theory"} \\ - @{command_def "defs"} & : & @{text "theory \ 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 \ 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 \ theory"} & (axiomatic!) \\ - \end{matharray} - @{rail " @@{command oracle} @{syntax name} '=' @{syntax text} "} diff -r a83b25e5bad3 -r 3f704717a67f doc-src/IsarRef/Thy/document/Spec.tex --- 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}}}}}[]