src/Cube/ROOT
author wenzelm
Tue Aug 12 21:29:50 2014 +0200 (2014-08-12)
changeset 57920 c1953856cfca
parent 51403 2ff3a5589b05
child 66946 3d8fd98c7c86
permissions -rw-r--r--
clarified focus and key handling -- more like SideKick;
avoid resetting input map with its potentially confusion propagation of key events to unrelated components, e.g. main text area or tree scrollbar;
wenzelm@51397
     1
chapter Cube
wenzelm@51397
     2
wenzelm@48738
     3
session Cube = Pure +
wenzelm@48475
     4
  description {*
wenzelm@48475
     5
    Author:     Tobias Nipkow
wenzelm@48475
     6
    Copyright   1992  University of Cambridge
wenzelm@48475
     7
wenzelm@51403
     8
    Barendregt's Lambda-Cube.
wenzelm@51403
     9
wenzelm@51403
    10
    NB: the formalization is not completely sound!  It does not enforce
wenzelm@51403
    11
    distinctness of variable names in contexts!
wenzelm@51403
    12
wenzelm@51403
    13
    For more information about the Lambda-Cube, see H. Barendregt, Introduction
wenzelm@51403
    14
    to Generalised Type Systems, J. Functional Programming.
wenzelm@48475
    15
  *}
wenzelm@48483
    16
  options [document = false]
wenzelm@48475
    17
  theories Example
wenzelm@48475
    18