equal
deleted
inserted
replaced
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1994 University of Cambridge |
4 Copyright 1994 University of Cambridge |
5 *) |
5 *) |
6 |
6 |
7 header {* |
7 header {* The accessible part of a relation *} |
8 \title{The accessible part of a relation} |
|
9 \author{Lawrence C Paulson} |
|
10 *} |
|
11 |
8 |
12 theory Accessible_Part = Main: |
9 theory Accessible_Part = Main: |
13 |
10 |
14 |
11 |
15 subsection {* Inductive definition *} |
12 subsection {* Inductive definition *} |