equal
deleted
inserted
replaced
1 (* Title: FOL/ex/int |
1 (* Title: FOLP/ex/int.ML |
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 Intuitionistic First-Order Logic |
6 Intuitionistic First-Order Logic |
13 by (Int.safe_tac 1); |
13 by (Int.safe_tac 1); |
14 by (Int.mp_tac 1); |
14 by (Int.mp_tac 1); |
15 by (Int.fast_tac 1); |
15 by (Int.fast_tac 1); |
16 *) |
16 *) |
17 |
17 |
18 writeln"File FOL/ex/int."; |
18 writeln"File FOLP/ex/int.ML"; |
19 |
19 |
20 (*Note: for PROPOSITIONAL formulae... |
20 (*Note: for PROPOSITIONAL formulae... |
21 ~A is classically provable iff it is intuitionistically provable. |
21 ~A is classically provable iff it is intuitionistically provable. |
22 Therefore A is classically provable iff ~~A is intuitionistically provable. |
22 Therefore A is classically provable iff ~~A is intuitionistically provable. |
23 |
23 |