
diff -r 14582233d36b -r 3d3e6e07b931 doc-src/IsarRef/Thy/pure.thy
--- 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}
 *}
 




