author | wenzelm |
Sun, 24 Mar 2019 17:23:48 +0100 | |
changeset 69964 | 699ffc7cbab8 |
parent 69319 | baccaf89ca0d |
child 70675 | efd995488228 |
permissions | -rw-r--r-- |
51397
03b586ee5930
support for 'chapter' specifications within session ROOT;
wenzelm
parents:
48738
diff
changeset
|
1 |
chapter LCF |
03b586ee5930
support for 'chapter' specifications within session ROOT;
wenzelm
parents:
48738
diff
changeset
|
2 |
|
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48483
diff
changeset
|
3 |
session LCF = Pure + |
69319 | 4 |
description " |
48475 | 5 |
Author: Tobias Nipkow |
6 |
Copyright 1992 University of Cambridge |
|
51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
7 |
|
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
8 |
Logic for Computable Functions. |
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
9 |
|
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
10 |
Useful references on LCF: Lawrence C. Paulson, |
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
11 |
Logic and Computation: Interactive proof with Cambridge LCF (CUP, 1987) |
69319 | 12 |
" |
66444 | 13 |
sessions |
14 |
FOL |
|
58974 | 15 |
theories |
16 |
LCF |
|
17 |
(* Some examples from Lawrence Paulson's book Logic and Computation *) |
|
18 |
"ex/Ex1" |
|
19 |
"ex/Ex2" |
|
20 |
"ex/Ex3" |
|
21 |
"ex/Ex4" |