| author | haftmann | 
| Fri, 14 Jun 2019 08:34:28 +0000 | |
| changeset 70347 | e5cd5471c18a | 
| 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"  |