equal
deleted
inserted
replaced
1 (* Title: CTT/ex/Elimination.thy |
1 (* Title: CTT/ex/Elimination.thy |
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1991 University of Cambridge |
3 Copyright 1991 University of Cambridge |
5 |
4 |
6 Some examples taken from P. Martin-L\"of, Intuitionistic type theory |
5 Some examples taken from P. Martin-L\"of, Intuitionistic type theory |
7 (Bibliopolis, 1984). |
6 (Bibliopolis, 1984). |
8 *) |
7 *) |
9 |
8 |
10 header "Examples with elimination rules" |
9 header "Examples with elimination rules" |
11 |
10 |
12 theory Elimination |
11 theory Elimination |