src/HOL/AxClasses/Semigroups.thy
author haftmann
Mon Aug 14 13:46:06 2006 +0200 (2006-08-14)
changeset 20380 14f9f2a1caa6
parent 16417 9bc16273c2d4
permissions -rw-r--r--
simplified code generator setup
wenzelm@10134
     1
(*  Title:      HOL/AxClasses/Semigroups.thy
wenzelm@10134
     2
    ID:         $Id$
wenzelm@10134
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@10134
     4
*)
wenzelm@10134
     5
haftmann@16417
     6
theory Semigroups imports Main begin
wenzelm@10134
     7
wenzelm@10134
     8
consts
wenzelm@10134
     9
  times :: "'a => 'a => 'a"    (infixl "[*]" 70)
wenzelm@10134
    10
wenzelm@12338
    11
axclass semigroup < type
wenzelm@10134
    12
  assoc: "(x [*] y) [*] z = x [*] (y [*] z)"
wenzelm@10134
    13
wenzelm@10134
    14
wenzelm@10134
    15
consts
wenzelm@10134
    16
  plus :: "'a => 'a => 'a"    (infixl "[+]" 70)
wenzelm@10134
    17
wenzelm@12338
    18
axclass plus_semigroup < type
wenzelm@10134
    19
  assoc: "(x [+] y) [+] z = x [+] (y [+] z)"
wenzelm@10134
    20
wenzelm@10134
    21
end