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