equal
deleted
inserted
replaced
26 by (fast_tac HOL_cs 1); |
26 by (fast_tac HOL_cs 1); |
27 qed "bool_commut"; |
27 qed "bool_commut"; |
28 |
28 |
29 |
29 |
30 (* cartesian products *) |
30 (* cartesian products *) |
|
31 |
|
32 val prod_ss = simpset_of "Prod"; |
31 |
33 |
32 goalw thy [times_prod_def] "(x * y) * z = x * (y * (z::'a::semigroup*'b::semigroup))"; |
34 goalw thy [times_prod_def] "(x * y) * z = x * (y * (z::'a::semigroup*'b::semigroup))"; |
33 by (simp_tac (prod_ss addsimps [assoc]) 1); |
35 by (simp_tac (prod_ss addsimps [assoc]) 1); |
34 qed "prod_assoc"; |
36 qed "prod_assoc"; |
35 |
37 |