author | wenzelm |
Mon, 03 Nov 1997 12:24:13 +0100 | |
changeset 4091 | 771b1f6422a8 |
parent 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 {| SIMPSET' (fn ss => simp_tac (ss addsimps [assoc])) 1 |} end