equal
deleted
inserted
replaced
3 Author: Olaf Müller |
3 Author: Olaf Müller |
4 License: GPL (GNU GENERAL PUBLIC LICENSE) |
4 License: GPL (GNU GENERAL PUBLIC LICENSE) |
5 *) |
5 *) |
6 |
6 |
7 (* Logic *) |
7 (* Logic *) |
8 |
|
9 val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R"; |
|
10 by (fast_tac (claset() addDs prems) 1); |
|
11 qed "imp_conj_lemma"; |
|
12 |
8 |
13 goal HOL.thy "(~(A&B)) = ((~A)&B| ~B)"; |
9 goal HOL.thy "(~(A&B)) = ((~A)&B| ~B)"; |
14 by (Fast_tac 1); |
10 by (Fast_tac 1); |
15 val and_de_morgan_and_absorbe = result(); |
11 val and_de_morgan_and_absorbe = result(); |
16 |
12 |