equal
deleted
inserted
replaced
1 (* Title: FOLP/ifol.ML |
1 (* Title: FOLP/IFOLP.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Martin D Coen, Cambridge University Computer Laboratory |
4 Copyright 1992 University of Cambridge |
4 Copyright 1992 University of Cambridge |
5 |
5 |
6 Tactics and lemmas for ifol.thy (intuitionistic first-order logic) |
6 Tactics and lemmas for IFOLP (Intuitionistic First-Order Logic with Proofs) |
7 *) |
7 *) |
8 |
8 |
9 open IFOLP; |
9 open IFOLP; |
10 |
10 |
11 signature IFOLP_LEMMAS = |
11 signature IFOLP_LEMMAS = |