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