equal
deleted
inserted
replaced
1 (* Title: FOL/fol.ML |
1 (* Title: FOLP/FOLP.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 1991 University of Cambridge |
4 Copyright 1991 University of Cambridge |
5 |
5 |
6 Tactics and lemmas for fol.thy (classical First-Order Logic) |
6 Tactics and lemmas for FOLP (Classical First-Order Logic with Proofs) |
7 *) |
7 *) |
8 |
8 |
9 open FOLP; |
9 open FOLP; |
10 |
10 |
11 signature FOLP_LEMMAS = |
11 signature FOLP_LEMMAS = |