doc-src/IsarImplementation/Thy/unused.thy
changeset 20470 c839b38a1f32
parent 20460 351c63bb2704
child 20474 af069653f1d7
     1.1 --- a/doc-src/IsarImplementation/Thy/unused.thy	Mon Sep 04 15:27:30 2006 +0200
     1.2 +++ b/doc-src/IsarImplementation/Thy/unused.thy	Mon Sep 04 16:28:27 2006 +0200
     1.3 @@ -1,6 +1,17 @@
     1.4  
     1.5  text {*
     1.6  
     1.7 +  
     1.8 +
     1.9 +  A \emph{fixed variable} acts like a local constant in the current
    1.10 +  context, representing some simple type @{text "\<alpha>"}, or some value
    1.11 +  @{text "x: \<tau>"} (for a fixed type expression @{text "\<tau>"}).  A
    1.12 +  \emph{schematic variable} acts like a placeholder for arbitrary
    1.13 +  elements, similar to outermost quantification.  The division between
    1.14 +  fixed and schematic variables tells which abstract entities are
    1.15 +  inside and outside the current context.
    1.16 +
    1.17 +
    1.18    @{index_ML Variable.trade: "Proof.context -> (thm list -> thm list) -> thm list -> thm list"} \\
    1.19  
    1.20