equal
deleted
inserted
replaced
4 Copyright 1991 University of Cambridge |
4 Copyright 1991 University of Cambridge |
5 |
5 |
6 First-Order Logic: propositional examples (intuitionistic and classical) |
6 First-Order Logic: propositional 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 |
|
10 ML_Context.set_context (SOME (Context.Theory thy)); |
|
11 |
9 |
12 |
10 writeln"commutative laws of & and | "; |
13 writeln"commutative laws of & and | "; |
11 Goal "?p : P & Q --> Q & P"; |
14 Goal "?p : P & Q --> Q & P"; |
12 by tac; |
15 by tac; |
13 result(); |
16 result(); |