author | wenzelm |
Fri, 01 Sep 1995 14:27:36 +0200 | |
changeset 1247 | 18b1441fb603 |
child 1266 | 3ae9fe3c0f68 |
permissions | -rw-r--r-- |
(* 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 (prod_ss addsimps [assoc]) 1 |} end