--- a/doc-src/IsarRef/Thy/pure.thy Mon Jun 02 22:50:21 2008 +0200
+++ b/doc-src/IsarRef/Thy/pure.thy Mon Jun 02 22:50:23 2008 +0200
@@ -6,629 +6,6 @@
chapter {* Basic language elements \label{ch:pure-syntax} *}
-text {*
- Subsequently, we introduce the main part of Pure theory and proof
- commands, together with fundamental proof methods and attributes.
- \Chref{ch:gen-tools} describes further Isar elements provided by
- generic tools and packages (such as the Simplifier) that are either
- part of Pure Isabelle or pre-installed in most object logics.
- Specific language elements introduced by the major object-logics are
- described in \chref{ch:hol} (Isabelle/HOL), \chref{ch:holcf}
- (Isabelle/HOLCF), and \chref{ch:zf} (Isabelle/ZF). Nevertheless,
- examples given in the generic parts will usually refer to
- Isabelle/HOL as well.
-
- \medskip Isar commands may be either \emph{proper} document
- constructors, or \emph{improper commands}. Some proof methods and
- attributes introduced later are classified as improper as well.
- Improper Isar language elements, which are subsequently marked by
- ``@{text "\<^sup>*"}'', are often helpful when developing proof
- documents, while their use is discouraged for the final
- human-readable outcome. Typical examples are diagnostic commands
- that print terms or theorems according to the current context; other
- commands emulate old-style tactical theorem proving.
-*}
-
-
-section {* Theory commands *}
-
-subsection {* Markup commands \label{sec:markup-thy} *}
-
-text {*
- \begin{matharray}{rcl}
- @{command_def "chapter"} & : & \isarkeep{local{\dsh}theory} \\
- @{command_def "section"} & : & \isarkeep{local{\dsh}theory} \\
- @{command_def "subsection"} & : & \isarkeep{local{\dsh}theory} \\
- @{command_def "subsubsection"} & : & \isarkeep{local{\dsh}theory} \\
- @{command_def "text"} & : & \isarkeep{local{\dsh}theory} \\
- @{command_def "text_raw"} & : & \isarkeep{local{\dsh}theory} \\
- \end{matharray}
-
- Apart from formal comments (see \secref{sec:comments}), markup
- commands provide a structured way to insert text into the document
- generated from a theory (see \cite{isabelle-sys} for more
- information on Isabelle's document preparation tools).
-
- \begin{rail}
- ('chapter' | 'section' | 'subsection' | 'subsubsection' | 'text') target? text
- ;
- 'text\_raw' text
- ;
- \end{rail}
-
- \begin{descr}
-
- \item [@{command "chapter"}, @{command "section"}, @{command
- "subsection"}, and @{command "subsubsection"}] mark chapter and
- section headings.
-
- \item [@{command "text"}] specifies paragraphs of plain text.
-
- \item [@{command "text_raw"}] inserts {\LaTeX} source into the
- output, without additional markup. Thus the full range of document
- manipulations becomes available.
-
- \end{descr}
-
- The @{text "text"} argument of these markup commands (except for
- @{command "text_raw"}) may contain references to formal entities
- (``antiquotations'', see also \secref{sec:antiq}). These are
- interpreted in the present theory context, or the named @{text
- "target"}.
-
- Any of these markup elements corresponds to a {\LaTeX} command with
- the name prefixed by @{verbatim "\\isamarkup"}. For the sectioning
- commands this is a plain macro with a single argument, e.g.\
- @{verbatim "\\isamarkupchapter{"}@{text "\<dots>"}@{verbatim "}"} for
- @{command "chapter"}. The @{command "text"} markup results in a
- {\LaTeX} environment @{verbatim "\\begin{isamarkuptext}"} @{text
- "\<dots>"} @{verbatim "\\end{isamarkuptext}"}, while @{command "text_raw"}
- causes the text to be inserted directly into the {\LaTeX} source.
-
- \medskip Additional markup commands are available for proofs (see
- \secref{sec:markup-prf}). Also note that the @{command_ref
- "header"} declaration (see \secref{sec:begin-thy}) admits to insert
- section markup just preceding the actual theory definition.
-*}
-
-
-subsection {* Type classes and sorts \label{sec:classes} *}
-
-text {*
- \begin{matharray}{rcll}
- @{command_def "classes"} & : & \isartrans{theory}{theory} \\
- @{command_def "classrel"} & : & \isartrans{theory}{theory} & (axiomatic!) \\
- @{command_def "defaultsort"} & : & \isartrans{theory}{theory} \\
- @{command_def "class_deps"} & : & \isarkeep{theory~|~proof} \\
- \end{matharray}
-
- \begin{rail}
- 'classes' (classdecl +)
- ;
- 'classrel' (nameref ('<' | subseteq) nameref + 'and')
- ;
- 'defaultsort' sort
- ;
- \end{rail}
-
- \begin{descr}
-
- \item [@{command "classes"}~@{text "c \<subseteq> c\<^sub>1, \<dots>, c\<^sub>n"}]
- declares class @{text c} to be a subclass of existing classes @{text
- "c\<^sub>1, \<dots>, c\<^sub>n"}. Cyclic class structures are not permitted.
-
- \item [@{command "classrel"}~@{text "c\<^sub>1 \<subseteq> c\<^sub>2"}] states
- subclass relations between existing classes @{text "c\<^sub>1"} and
- @{text "c\<^sub>2"}. This is done axiomatically! The @{command_ref
- "instance"} command (see \secref{sec:axclass}) provides a way to
- introduce proven class relations.
-
- \item [@{command "defaultsort"}~@{text s}] makes sort @{text s} the
- new default sort for any type variables given without sort
- constraints. Usually, the default sort would be only changed when
- defining a new object-logic.
-
- \item [@{command "class_deps"}] visualizes the subclass relation,
- using Isabelle's graph browser tool (see also \cite{isabelle-sys}).
-
- \end{descr}
-*}
-
-
-subsection {* Primitive types and type abbreviations \label{sec:types-pure} *}
-
-text {*
- \begin{matharray}{rcll}
- @{command_def "types"} & : & \isartrans{theory}{theory} \\
- @{command_def "typedecl"} & : & \isartrans{theory}{theory} \\
- @{command_def "nonterminals"} & : & \isartrans{theory}{theory} \\
- @{command_def "arities"} & : & \isartrans{theory}{theory} & (axiomatic!) \\
- \end{matharray}
-
- \begin{rail}
- 'types' (typespec '=' type infix? +)
- ;
- 'typedecl' typespec infix?
- ;
- 'nonterminals' (name +)
- ;
- 'arities' (nameref '::' arity +)
- ;
- \end{rail}
-
- \begin{descr}
-
- \item [@{command "types"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t = \<tau>"}]
- introduces \emph{type synonym} @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"}
- for existing type @{text "\<tau>"}. Unlike actual type definitions, as
- are available in Isabelle/HOL for example, type synonyms are just
- purely syntactic abbreviations without any logical significance.
- Internally, type synonyms are fully expanded.
-
- \item [@{command "typedecl"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"}]
- declares a new type constructor @{text t}, intended as an actual
- logical type (of the object-logic, if available).
-
- \item [@{command "nonterminals"}~@{text c}] declares type
- constructors @{text c} (without arguments) to act as purely
- syntactic types, i.e.\ nonterminal symbols of Isabelle's inner
- syntax of terms or types.
-
- \item [@{command "arities"}~@{text "t :: (s\<^sub>1, \<dots>, s\<^sub>n)
- s"}] augments Isabelle's order-sorted signature of types by new type
- constructor arities. This is done axiomatically! The @{command_ref
- "instance"} command (see \S\ref{sec:axclass}) provides a way to
- introduce proven type arities.
-
- \end{descr}
-*}
-
-
-subsection {* Primitive constants and definitions \label{sec:consts} *}
-
-text {*
- 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
- where the arguments of @{text c} appear on the left, abbreviating a
- prefix of @{text \<lambda>}-abstractions, e.g.\ @{text "c \<equiv> \<lambda>x y. t"} may be
- written more conveniently as @{text "c x y \<equiv> t"}. Moreover,
- definitions may be weakened by adding arbitrary pre-conditions:
- @{text "A \<Longrightarrow> c x y \<equiv> t"}.
-
- \medskip The built-in well-formedness conditions for definitional
- specifications are:
-
- \begin{itemize}
-
- \item Arguments (on the left-hand side) must be distinct variables.
-
- \item All variables on the right-hand side must also appear on the
- left-hand side.
-
- \item All type variables on the right-hand side must also appear on
- the left-hand side; this prohibits @{text "0 :: nat \<equiv> length ([] ::
- \<alpha> list)"} for example.
-
- \item The definition must not be recursive. Most object-logics
- provide definitional principles that can be used to express
- recursion safely.
-
- \end{itemize}
-
- Overloading means that a constant being declared as @{text "c :: \<alpha>
- decl"} may be defined separately on type instances @{text "c ::
- (\<beta>\<^sub>1, \<dots>, \<beta>\<^sub>n) t decl"} for each type constructor @{text
- t}. The right-hand side may mention overloaded constants
- recursively at type instances corresponding to the immediate
- argument types @{text "\<beta>\<^sub>1, \<dots>, \<beta>\<^sub>n"}. Incomplete
- specification patterns impose global constraints on all occurrences,
- e.g.\ @{text "d :: \<alpha> \<times> \<alpha>"} on the left-hand side means that all
- 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"} & : & \isartrans{theory}{theory} \\
- @{command_def "defs"} & : & \isartrans{theory}{theory} \\
- @{command_def "constdefs"} & : & \isartrans{theory}{theory} \\
- \end{matharray}
-
- \begin{rail}
- 'consts' ((name '::' type mixfix?) +)
- ;
- 'defs' ('(' 'unchecked'? 'overloaded'? ')')? \\ (axmdecl prop +)
- ;
- \end{rail}
-
- \begin{rail}
- 'constdefs' structs? (constdecl? constdef +)
- ;
-
- structs: '(' 'structure' (vars + 'and') ')'
- ;
- constdecl: ((name '::' type mixfix | name '::' type | name mixfix) 'where'?) | name 'where'
- ;
- constdef: thmdecl? prop
- ;
- \end{rail}
-
- \begin{descr}
-
- \item [@{command "consts"}~@{text "c :: \<sigma>"}] declares constant
- @{text c} to have any instance of type scheme @{text \<sigma>}. The
- optional mixfix annotations may attach concrete syntax to the
- constants declared.
-
- \item [@{command "defs"}~@{text "name: eqn"}] introduces @{text eqn}
- as a definitional axiom for some existing constant.
-
- The @{text "(unchecked)"} option disables global dependency checks
- for this definition, which is occasionally useful for exotic
- overloading. It is at the discretion of the user to avoid malformed
- theory specifications!
-
- The @{text "(overloaded)"} option declares definitions to be
- potentially overloaded. Unless this option is given, a warning
- message would be issued for any definitional equation with a more
- special type than that of the corresponding constant declaration.
-
- \item [@{command "constdefs"}] provides a streamlined combination of
- constants declarations and definitions: type-inference takes care of
- the most general typing of the given specification (the optional
- type constraint may refer to type-inference dummies ``@{text
- _}'' as usual). The resulting type declaration needs to agree with
- that of the specification; overloading is \emph{not} supported here!
-
- The constant name may be omitted altogether, if neither type nor
- syntax declarations are given. The canonical name of the
- definitional axiom for constant @{text c} will be @{text c_def},
- unless specified otherwise. Also note that the given list of
- specifications is processed in a strictly sequential manner, with
- type-checking being performed independently.
-
- An optional initial context of @{text "(structure)"} declarations
- admits use of indexed syntax, using the special symbol @{verbatim
- "\<index>"} (printed as ``@{text "\<index>"}''). The latter concept is
- particularly useful with locales (see also \S\ref{sec:locale}).
-
- \end{descr}
-*}
-
-
-subsection {* Syntax and translations \label{sec:syn-trans} *}
-
-text {*
- \begin{matharray}{rcl}
- @{command_def "syntax"} & : & \isartrans{theory}{theory} \\
- @{command_def "no_syntax"} & : & \isartrans{theory}{theory} \\
- @{command_def "translations"} & : & \isartrans{theory}{theory} \\
- @{command_def "no_translations"} & : & \isartrans{theory}{theory} \\
- \end{matharray}
-
- \begin{rail}
- ('syntax' | 'no\_syntax') mode? (constdecl +)
- ;
- ('translations' | 'no\_translations') (transpat ('==' | '=>' | '<=' | rightleftharpoons | rightharpoonup | leftharpoondown) transpat +)
- ;
-
- mode: ('(' ( name | 'output' | name 'output' ) ')')
- ;
- transpat: ('(' nameref ')')? string
- ;
- \end{rail}
-
- \begin{descr}
-
- \item [@{command "syntax"}~@{text "(mode) decls"}] is similar to
- @{command "consts"}~@{text decls}, except that the actual logical
- signature extension is omitted. Thus the context free grammar of
- Isabelle's inner syntax may be augmented in arbitrary ways,
- independently of the logic. The @{text mode} argument refers to the
- print mode that the grammar rules belong; unless the @{keyword_ref
- "output"} indicator is given, all productions are added both to the
- input and output grammar.
-
- \item [@{command "no_syntax"}~@{text "(mode) decls"}] removes
- grammar declarations (and translations) resulting from @{text
- decls}, which are interpreted in the same manner as for @{command
- "syntax"} above.
-
- \item [@{command "translations"}~@{text rules}] specifies syntactic
- translation rules (i.e.\ macros): parse~/ print rules (@{text "\<rightleftharpoons>"}),
- parse rules (@{text "\<rightharpoonup>"}), or print rules (@{text "\<leftharpoondown>"}).
- Translation patterns may be prefixed by the syntactic category to be
- used for parsing; the default is @{text logic}.
-
- \item [@{command "no_translations"}~@{text rules}] removes syntactic
- translation rules, which are interpreted in the same manner as for
- @{command "translations"} above.
-
- \end{descr}
-*}
-
-
-subsection {* Axioms and theorems \label{sec:axms-thms} *}
-
-text {*
- \begin{matharray}{rcll}
- @{command_def "axioms"} & : & \isartrans{theory}{theory} & (axiomatic!) \\
- @{command_def "lemmas"} & : & \isarkeep{local{\dsh}theory} \\
- @{command_def "theorems"} & : & isarkeep{local{\dsh}theory} \\
- \end{matharray}
-
- \begin{rail}
- 'axioms' (axmdecl prop +)
- ;
- ('lemmas' | 'theorems') target? (thmdef? thmrefs + 'and')
- ;
- \end{rail}
-
- \begin{descr}
-
- \item [@{command "axioms"}~@{text "a: \<phi>"}] introduces arbitrary
- statements as axioms of the meta-logic. In fact, axioms are
- ``axiomatic theorems'', and may be referred later just as any other
- theorem.
-
- Axioms are usually only introduced when declaring new logical
- systems. Everyday work is typically done the hard way, with proper
- definitions and proven theorems.
-
- \item [@{command "lemmas"}~@{text "a = b\<^sub>1 \<dots> b\<^sub>n"}]
- retrieves and stores existing facts in the theory context, or the
- specified target context (see also \secref{sec:target}). Typical
- applications would also involve attributes, to declare Simplifier
- rules, for example.
-
- \item [@{command "theorems"}] is essentially the same as @{command
- "lemmas"}, but marks the result as a different kind of facts.
-
- \end{descr}
-*}
-
-
-subsection {* Name spaces *}
-
-text {*
- \begin{matharray}{rcl}
- @{command_def "global"} & : & \isartrans{theory}{theory} \\
- @{command_def "local"} & : & \isartrans{theory}{theory} \\
- @{command_def "hide"} & : & \isartrans{theory}{theory} \\
- \end{matharray}
-
- \begin{rail}
- 'hide' ('(open)')? name (nameref + )
- ;
- \end{rail}
-
- Isabelle organizes any kind of name declarations (of types,
- constants, theorems etc.) by separate hierarchically structured name
- spaces. Normally the user does not have to control the behavior of
- name spaces by hand, yet the following commands provide some way to
- do so.
-
- \begin{descr}
-
- \item [@{command "global"} and @{command "local"}] change the
- current name declaration mode. Initially, theories start in
- @{command "local"} mode, causing all names to be automatically
- qualified by the theory name. Changing this to @{command "global"}
- causes all names to be declared without the theory prefix, until
- @{command "local"} is declared again.
-
- Note that global names are prone to get hidden accidently later,
- when qualified names of the same base name are introduced.
-
- \item [@{command "hide"}~@{text "space names"}] fully removes
- declarations from a given name space (which may be @{text "class"},
- @{text "type"}, @{text "const"}, or @{text "fact"}); with the @{text
- "(open)"} option, only the base name is hidden. Global
- (unqualified) names may never be hidden.
-
- Note that hiding name space accesses has no impact on logical
- declarations -- they remain valid internally. Entities that are no
- longer accessible to the user are printed with the special qualifier
- ``@{text "??"}'' prefixed to the full internal name.
-
- \end{descr}
-*}
-
-
-subsection {* Incorporating ML code \label{sec:ML} *}
-
-text {*
- \begin{matharray}{rcl}
- @{command_def "use"} & : & \isarkeep{theory~|~local{\dsh}theory} \\
- @{command_def "ML"} & : & \isarkeep{theory~|~local{\dsh}theory} \\
- @{command_def "ML_val"} & : & \isartrans{\cdot}{\cdot} \\
- @{command_def "ML_command"} & : & \isartrans{\cdot}{\cdot} \\
- @{command_def "setup"} & : & \isartrans{theory}{theory} \\
- @{command_def "method_setup"} & : & \isartrans{theory}{theory} \\
- \end{matharray}
-
- \begin{rail}
- 'use' name
- ;
- ('ML' | 'ML\_val' | 'ML\_command' | 'setup') text
- ;
- 'method\_setup' name '=' text text
- ;
- \end{rail}
-
- \begin{descr}
-
- \item [@{command "use"}~@{text "file"}] reads and executes ML
- commands from @{text "file"}. The current theory context is passed
- down to the ML toplevel and may be modified, using @{ML
- "Context.>>"} or derived ML commands. The file name is checked with
- the @{keyword_ref "uses"} dependency declaration given in the theory
- header (see also \secref{sec:begin-thy}).
-
- \item [@{command "ML"}~@{text "text"}] is similar to @{command
- "use"}, but executes ML commands directly from the given @{text
- "text"}.
-
- \item [@{command "ML_val"} and @{command "ML_command"}] are
- diagnostic versions of @{command "ML"}, which means that the context
- may not be updated. @{command "ML_val"} echos the bindings produced
- at the ML toplevel, but @{command "ML_command"} is silent.
-
- \item [@{command "setup"}~@{text "text"}] changes the current theory
- context by applying @{text "text"}, which refers to an ML expression
- of type @{ML_type "theory -> theory"}. This enables to initialize
- any object-logic specific tools and packages written in ML, for
- example.
-
- \item [@{command "method_setup"}~@{text "name = text description"}]
- defines a proof method in the current theory. The given @{text
- "text"} has to be an ML expression of type @{ML_type "Args.src ->
- Proof.context -> Proof.method"}. Parsing concrete method syntax
- from @{ML_type Args.src} input can be quite tedious in general. The
- following simple examples are for methods without any explicit
- arguments, or a list of theorems, respectively.
-
-%FIXME proper antiquotations
-{\footnotesize
-\begin{verbatim}
- Method.no_args (Method.METHOD (fn facts => foobar_tac))
- Method.thms_args (fn thms => Method.METHOD (fn facts => foobar_tac))
- Method.ctxt_args (fn ctxt => Method.METHOD (fn facts => foobar_tac))
- Method.thms_ctxt_args (fn thms => fn ctxt =>
- Method.METHOD (fn facts => foobar_tac))
-\end{verbatim}
-}
-
- Note that mere tactic emulations may ignore the @{text facts}
- parameter above. Proper proof methods would do something
- appropriate with the list of current facts, though. Single-rule
- methods usually do strict forward-chaining (e.g.\ by using @{ML
- Drule.multi_resolves}), while automatic ones just insert the facts
- using @{ML Method.insert_tac} before applying the main tactic.
-
- \end{descr}
-*}
-
-
-subsection {* Syntax translation functions *}
-
-text {*
- \begin{matharray}{rcl}
- @{command_def "parse_ast_translation"} & : & \isartrans{theory}{theory} \\
- @{command_def "parse_translation"} & : & \isartrans{theory}{theory} \\
- @{command_def "print_translation"} & : & \isartrans{theory}{theory} \\
- @{command_def "typed_print_translation"} & : & \isartrans{theory}{theory} \\
- @{command_def "print_ast_translation"} & : & \isartrans{theory}{theory} \\
- @{command_def "token_translation"} & : & \isartrans{theory}{theory} \\
- \end{matharray}
-
- \begin{rail}
- ( 'parse\_ast\_translation' | 'parse\_translation' | 'print\_translation' |
- 'typed\_print\_translation' | 'print\_ast\_translation' ) ('(advanced)')? text
- ;
-
- 'token\_translation' text
- ;
- \end{rail}
-
- Syntax translation functions written in ML admit almost arbitrary
- manipulations of Isabelle's inner syntax. Any of the above commands
- have a single \railqtok{text} argument that refers to an ML
- expression of appropriate type, which are as follows by default:
-
-%FIXME proper antiquotations
-\begin{ttbox}
-val parse_ast_translation : (string * (ast list -> ast)) list
-val parse_translation : (string * (term list -> term)) list
-val print_translation : (string * (term list -> term)) list
-val typed_print_translation :
- (string * (bool -> typ -> term list -> term)) list
-val print_ast_translation : (string * (ast list -> ast)) list
-val token_translation :
- (string * string * (string -> string * real)) list
-\end{ttbox}
-
- If the @{text "(advanced)"} option is given, the corresponding
- translation functions may depend on the current theory or proof
- context. This allows to implement advanced syntax mechanisms, as
- translations functions may refer to specific theory declarations or
- auxiliary proof data.
-
- See also \cite[\S8]{isabelle-ref} for more information on the
- general concept of syntax transformations in Isabelle.
-
-%FIXME proper antiquotations
-\begin{ttbox}
-val parse_ast_translation:
- (string * (Context.generic -> ast list -> ast)) list
-val parse_translation:
- (string * (Context.generic -> term list -> term)) list
-val print_translation:
- (string * (Context.generic -> term list -> term)) list
-val typed_print_translation:
- (string * (Context.generic -> bool -> typ -> term list -> term)) list
-val print_ast_translation:
- (string * (Context.generic -> ast list -> ast)) list
-\end{ttbox}
-*}
-
-
-subsection {* Oracles *}
-
-text {*
- \begin{matharray}{rcl}
- @{command_def "oracle"} & : & \isartrans{theory}{theory} \\
- \end{matharray}
-
- The oracle interface promotes a given ML function @{ML_text
- "theory -> T -> term"} to @{ML_text "theory -> T -> thm"}, for some
- type @{ML_text T} given by the user. This acts like an infinitary
- specification of axioms -- there is no internal check of the
- correctness of the results! The inference kernel records oracle
- invocations within the internal derivation object of theorems, and
- the pretty printer attaches ``@{text "[!]"}'' to indicate results
- that are not fully checked by Isabelle inferences.
-
- \begin{rail}
- 'oracle' name '(' type ')' '=' text
- ;
- \end{rail}
-
- \begin{descr}
-
- \item [@{command "oracle"}~@{text "name (type) = text"}] turns the
- given ML expression @{text "text"} of type
- @{ML_text "theory ->"}~@{text "type"}~@{ML_text "-> term"} into an
- ML function of type
- @{ML_text "theory ->"}~@{text "type"}~@{ML_text "-> thm"}, which is
- bound to the global identifier @{ML_text name}.
-
- \end{descr}
-*}
-
-
-section {* Proof commands *}
-
-subsection {* Markup commands \label{sec:markup-prf} *}
-
-text {*
- \begin{matharray}{rcl}
- @{command_def "sect"} & : & \isartrans{proof}{proof} \\
- @{command_def "subsect"} & : & \isartrans{proof}{proof} \\
- @{command_def "subsubsect"} & : & \isartrans{proof}{proof} \\
- @{command_def "txt"} & : & \isartrans{proof}{proof} \\
- @{command_def "txt_raw"} & : & \isartrans{proof}{proof} \\
- \end{matharray}
-
- These markup commands for proof mode closely correspond to the ones
- of theory mode (see \S\ref{sec:markup-thy}).
-
- \begin{rail}
- ('sect' | 'subsect' | 'subsubsect' | 'txt' | 'txt\_raw') text
- ;
- \end{rail}
-*}
-
-
section {* Other commands *}
subsection {* Diagnostics *}
@@ -846,15 +223,11 @@
@{command_def "cd"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\
@{command_def "pwd"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\
@{command_def "use_thy"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\
- @{command_def "display_drafts"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\
- @{command_def "print_drafts"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\
\end{matharray}
\begin{rail}
('cd' | 'use\_thy' | 'update\_thy') name
;
- ('display\_drafts' | 'print\_drafts') (name +)
- ;
\end{rail}
\begin{descr}
@@ -868,12 +241,6 @@
These system commands are scarcely used when working interactively,
since loading of theories is done automatically as required.
- \item [@{command "display_drafts"}~@{text paths} and @{command
- "print_drafts"}~@{text paths}] perform simple output of a given list
- of raw source files. Only those symbols that do not require
- additional {\LaTeX} packages are displayed properly, everything else
- is left verbatim.
-
\end{descr}
*}