doc-src/IsarImplementation/Thy/unused.thy
author wenzelm
Mon Sep 04 16:28:27 2006 +0200 (2006-09-04 ago)
changeset 20470 c839b38a1f32
parent 20460 351c63bb2704
child 20474 af069653f1d7
permissions -rw-r--r--
more on variables;
tuned;
     1 
     2 text {*
     3 
     4   
     5 
     6   A \emph{fixed variable} acts like a local constant in the current
     7   context, representing some simple type @{text "\<alpha>"}, or some value
     8   @{text "x: \<tau>"} (for a fixed type expression @{text "\<tau>"}).  A
     9   \emph{schematic variable} acts like a placeholder for arbitrary
    10   elements, similar to outermost quantification.  The division between
    11   fixed and schematic variables tells which abstract entities are
    12   inside and outside the current context.
    13 
    14 
    15   @{index_ML Variable.trade: "Proof.context -> (thm list -> thm list) -> thm list -> thm list"} \\
    16 
    17 
    18 
    19   \item @{ML Variable.trade} composes @{ML Variable.import} and @{ML
    20   Variable.export}, i.e.\ it provides a view on facts with all
    21   variables being fixed in the current context.
    22 
    23 
    24   In practice, super-contexts emerge either by merging existing ones,
    25   or by adding explicit declarations.  For example, new theories are
    26   usually derived by importing existing theories from the library
    27   @{text "\<Theta> = \<Theta>\<^sub>1 + \<dots> + \<Theta>\<^isub>n"}, or 
    28 
    29 
    30 
    31   The Isar toplevel works differently for interactive developments
    32   vs.\ batch processing of theory sources.  For example, diagnostic
    33   commands produce a warning batch mode, because they are considered
    34   alien to the final theory document being produced eventually.
    35   Moreover, full @{text undo} with intermediate checkpoints to protect
    36   against destroying theories accidentally are limited to interactive
    37   mode.  In batch mode there is only a single strictly linear stream
    38   of potentially desctructive theory transformations.
    39 
    40   \item @{ML Toplevel.empty} is an empty transition; the Isar command
    41   dispatcher internally applies @{ML Toplevel.name} (for the command)
    42   name and @{ML Toplevel.position} for the source position.
    43 
    44 *}
    45