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 Trivial Abstraction Example. |
6 Trivial Abstraction Example. |
7 *) |
7 *) |
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 |
|
13 |
8 |
14 Goalw [is_abstraction_def] |
9 Goalw [is_abstraction_def] |
15 "is_abstraction h_abs C_ioa A_ioa"; |
10 "is_abstraction h_abs C_ioa A_ioa"; |
16 by (rtac conjI 1); |
11 by (rtac conjI 1); |
17 (* ------------- start states ------------ *) |
12 (* ------------- start states ------------ *) |