doc-src/IsarImplementation/Thy/unused.thy
author wenzelm
Thu Sep 07 20:12:08 2006 +0200 (2006-09-07 ago)
changeset 20491 98ba42f19995
parent 20477 e623b0e30541
permissions -rw-r--r--
tuned;
     1 
     2 section {* Sessions and document preparation *}
     3 
     4 section {* Structured output *}
     5 
     6 subsection {* Pretty printing *}
     7 
     8 text FIXME
     9 
    10 subsection {* Output channels *}
    11 
    12 text FIXME
    13 
    14 subsection {* Print modes \label{sec:print-mode} *}
    15 
    16 text FIXME
    17 
    18 text {*
    19 
    20 
    21   \medskip The general concept supports block-structured reasoning
    22   nicely, with arbitrary mechanisms for introducing local assumptions.
    23   The common reasoning pattern is as follows:
    24 
    25   \medskip
    26   \begin{tabular}{l}
    27   @{text "add_assms e\<^isub>1 A\<^isub>1"} \\
    28   @{text "\<dots>"} \\
    29   @{text "add_assms e\<^isub>n A\<^isub>n"} \\
    30   @{text "export"} \\
    31   \end{tabular}
    32   \medskip
    33 
    34   \noindent The final @{text "export"} will turn any fact @{text
    35   "A\<^isub>1, \<dots>, A\<^isub>n \<turnstile> B"} into some @{text "\<turnstile> B'"}, by
    36   applying the export rules @{text "e\<^isub>1, \<dots>, e\<^isub>n"}
    37   inside-out.
    38   
    39 
    40   A \emph{fixed variable} acts like a local constant in the current
    41   context, representing some simple type @{text "\<alpha>"}, or some value
    42   @{text "x: \<tau>"} (for a fixed type expression @{text "\<tau>"}).  A
    43   \emph{schematic variable} acts like a placeholder for arbitrary
    44   elements, similar to outermost quantification.  The division between
    45   fixed and schematic variables tells which abstract entities are
    46   inside and outside the current context.
    47 
    48 
    49   @{index_ML Variable.trade: "Proof.context -> (thm list -> thm list) -> thm list -> thm list"} \\
    50 
    51 
    52 
    53   \item @{ML Variable.trade} composes @{ML Variable.import} and @{ML
    54   Variable.export}, i.e.\ it provides a view on facts with all
    55   variables being fixed in the current context.
    56 
    57 
    58   In practice, super-contexts emerge either by merging existing ones,
    59   or by adding explicit declarations.  For example, new theories are
    60   usually derived by importing existing theories from the library
    61   @{text "\<Theta> = \<Theta>\<^sub>1 + \<dots> + \<Theta>\<^isub>n"}, or 
    62 
    63 
    64 
    65   The Isar toplevel works differently for interactive developments
    66   vs.\ batch processing of theory sources.  For example, diagnostic
    67   commands produce a warning batch mode, because they are considered
    68   alien to the final theory document being produced eventually.
    69   Moreover, full @{text undo} with intermediate checkpoints to protect
    70   against destroying theories accidentally are limited to interactive
    71   mode.  In batch mode there is only a single strictly linear stream
    72   of potentially desctructive theory transformations.
    73 
    74   \item @{ML Toplevel.empty} is an empty transition; the Isar command
    75   dispatcher internally applies @{ML Toplevel.name} (for the command)
    76   name and @{ML Toplevel.position} for the source position.
    77 
    78 *}
    79