Various new lemmas. Improved conversion of equations to rewrite rules:
(s=t becomes (s=t)==True if s=t loops).
(* Title: HOL/AxClasses/Tutorial/ProdGroupInsts.thy
ID: $Id$
Author: Markus Wenzel, TU Muenchen
Lift constant "<*>" to cartesian products, then prove that the
'functor' "*" maps semigroups into semigroups.
*)
ProdGroupInsts = Prod + Group +
(* direct products of semigroups *)
defs
prod_prod_def "p <*> q == (fst p <*> fst q, snd p <*> snd q)"
instance
"*" :: (semigroup, semigroup) semigroup
{| simp_tac (!simpset addsimps [assoc]) 1 |}
end