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