equal
deleted
inserted
replaced
1 (* Title: FOL/ex/cla |
1 (* Title: FOL/ex/cla.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 1994 University of Cambridge |
4 Copyright 1994 University of Cambridge |
5 |
5 |
6 Classical First-Order Logic |
6 Classical First-Order Logic |
7 *) |
7 *) |
8 |
8 |
9 writeln"File FOL/ex/cla."; |
9 writeln"File FOL/ex/cla.ML"; |
10 |
10 |
11 open Cla; (*in case structure Int is open!*) |
11 open Cla; (*in case structure Int is open!*) |
12 |
12 |
13 goal FOL.thy "(P --> Q | R) --> (P-->Q) | (P-->R)"; |
13 goal FOL.thy "(P --> Q | R) --> (P-->Q) | (P-->R)"; |
14 by (fast_tac FOL_cs 1); |
14 by (fast_tac FOL_cs 1); |