equal
deleted
inserted
replaced
1 (* Title: CTT/ex/elim |
1 (* Title: CTT/ex/elim |
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 1991 University of Cambridge |
4 Copyright 1991 University of Cambridge |
5 |
5 |
6 SOME examples taken from P. Martin-L\"of, Intuitionistic type theory |
6 Some examples taken from P. Martin-L\"of, Intuitionistic type theory |
7 (Bibliopolis, 1984). |
7 (Bibliopolis, 1984). |
8 |
8 |
9 by (safe_tac prems 1); |
9 by (safe_tac prems 1); |
10 by (step_tac prems 1); |
10 by (step_tac prems 1); |
11 by (pc_tac prems 1); |
11 by (pc_tac prems 1); |