equal
deleted
inserted
replaced
9 *) |
9 *) |
10 |
10 |
11 open Enum; |
11 open Enum; |
12 |
12 |
13 goal Enum.thy "C00 ~= C01"; |
13 goal Enum.thy "C00 ~= C01"; |
14 by (simp_tac (!simpset addsimps enum.free_iffs) 1); |
14 by (simp_tac (simpset() addsimps enum.free_iffs) 1); |
15 result(); |
15 result(); |
16 |
16 |