equal
deleted
inserted
replaced
1 (* Title: FOL/ex/quant |
1 (* Title: FOLP/ex/quant.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 First-Order Logic: quantifier examples (intuitionistic and classical) |
6 First-Order Logic: quantifier examples (intuitionistic and classical) |
7 Needs declarations of the theory "thy" and the tactic "tac" |
7 Needs declarations of the theory "thy" and the tactic "tac" |
8 *) |
8 *) |
9 |
9 |
10 writeln"File FOL/ex/quant."; |
10 writeln"File FOLP/ex/quant.ML"; |
11 |
11 |
12 goal thy "?p : (ALL x y.P(x,y)) --> (ALL y x.P(x,y))"; |
12 goal thy "?p : (ALL x y.P(x,y)) --> (ALL y x.P(x,y))"; |
13 by tac; |
13 by tac; |
14 result(); |
14 result(); |
15 |
15 |