changeset 7 | 268f93ab3bc4 |
parent 0 | a5a9c433f639 |
child 38 | 4433428596f9 |
6:8ce8c4d13d4d | 7:268f93ab3bc4 |
---|---|
26 val monos = []; |
26 val monos = []; |
27 val type_intrs = data_typechecks |
27 val type_intrs = data_typechecks |
28 val type_elims = []); |
28 val type_elims = []); |
29 |
29 |
30 goal Enum.thy "~ con59=con60"; |
30 goal Enum.thy "~ con59=con60"; |
31 by (SIMP_TAC (ZF_ss addrews Enum.free_iffs) 1); (*2.3 secs*) |
31 by (simp_tac (ZF_ss addsimps Enum.free_iffs) 1); (*2.3 secs*) |
32 result(); |
32 result(); |
33 |
33 |