src/LCF/ROOT
author wenzelm
Tue Aug 12 21:29:50 2014 +0200 (2014-08-12)
changeset 57920 c1953856cfca
parent 51403 2ff3a5589b05
child 58974 cbc2ac19d783
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;
     1 chapter LCF
     2 
     3 session LCF = Pure +
     4   description {*
     5     Author:     Tobias Nipkow
     6     Copyright   1992  University of Cambridge
     7 
     8     Logic for Computable Functions.
     9 
    10     Useful references on LCF: Lawrence C. Paulson,
    11     Logic and Computation: Interactive proof with Cambridge LCF (CUP, 1987)
    12   *}
    13   options [document = false]
    14   theories LCF
    15 
    16 session "LCF-ex" in ex = LCF +
    17   description {*
    18     Author:     Tobias Nipkow
    19     Copyright   1991  University of Cambridge
    20 
    21     Some examples from Lawrence Paulson's book Logic and Computation.
    22   *}
    23   options [document = false]
    24   theories
    25     Ex1
    26     Ex2
    27     Ex3
    28     Ex4
    29