equal
deleted
inserted
replaced
1 (* Title: HOLCF/IOA/meta_theory/Seq.ML |
1 (* Title: HOLCF/IOA/meta_theory/Seq.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Olaf Müller |
3 Author: Olaf Mller |
4 *) |
4 *) |
5 |
5 |
6 Addsimps (sfinite.intrs @ seq.rews); |
6 Addsimps (sfinite.intrs @ seq.rews); |
7 |
7 |
8 |
8 |
9 (* Instead of adding UU_neq_nil every equation UU~=x could be changed to x~=UU *) |
9 (* Instead of adding UU_neq_nil every equation UU~=x could be changed to x~=UU *) |
|
10 (* |
10 Goal "UU ~=nil"; |
11 Goal "UU ~=nil"; |
11 by (res_inst_tac [("s1","UU"),("t1","nil")] (sym RS rev_contrapos) 1); |
12 by (res_inst_tac [("s1","UU"),("t1","nil")] (sym RS rev_contrapos) 1); |
12 by (REPEAT (Simp_tac 1)); |
13 by (REPEAT (Simp_tac 1)); |
13 qed"UU_neq_nil"; |
14 qed"UU_neq_nil"; |
14 |
15 |
15 Addsimps [UU_neq_nil]; |
16 Addsimps [UU_neq_nil]; |
16 |
17 *) |
17 |
18 |
18 |
19 |
19 |
20 |
20 (* ------------------------------------------------------------------------------------- *) |
21 (* ------------------------------------------------------------------------------------- *) |
21 |
22 |