isabelle: src/HOL/AxClasses/Semigroups.thy@50be659d4222 (annotated)

10134 537206cc738f moved axclass tutorial examples to top dir; wenzelm parents: diff changeset	1	(* Title: HOL/AxClasses/Semigroups.thy
537206cc738f moved axclass tutorial examples to top dir; wenzelm parents: diff changeset	2	ID: $Id$
537206cc738f moved axclass tutorial examples to top dir; wenzelm parents: diff changeset	3	Author: Markus Wenzel, TU Muenchen
537206cc738f moved axclass tutorial examples to top dir; wenzelm parents: diff changeset	4	*)
537206cc738f moved axclass tutorial examples to top dir; wenzelm parents: diff changeset	5
537206cc738f moved axclass tutorial examples to top dir; wenzelm parents: diff changeset	6	theory Semigroups = Main:
537206cc738f moved axclass tutorial examples to top dir; wenzelm parents: diff changeset	7
537206cc738f moved axclass tutorial examples to top dir; wenzelm parents: diff changeset	8	consts
537206cc738f moved axclass tutorial examples to top dir; wenzelm parents: diff changeset	9	times :: "'a => 'a => 'a" (infixl "[*]" 70)
537206cc738f moved axclass tutorial examples to top dir; wenzelm parents: diff changeset	10
537206cc738f moved axclass tutorial examples to top dir; wenzelm parents: diff changeset	11	axclass semigroup < "term"
537206cc738f moved axclass tutorial examples to top dir; wenzelm parents: diff changeset	12	assoc: "(x [] y) [] z = x [] (y [] z)"
537206cc738f moved axclass tutorial examples to top dir; wenzelm parents: diff changeset	13
537206cc738f moved axclass tutorial examples to top dir; wenzelm parents: diff changeset	14
537206cc738f moved axclass tutorial examples to top dir; wenzelm parents: diff changeset	15	consts
537206cc738f moved axclass tutorial examples to top dir; wenzelm parents: diff changeset	16	plus :: "'a => 'a => 'a" (infixl "[+]" 70)
537206cc738f moved axclass tutorial examples to top dir; wenzelm parents: diff changeset	17
537206cc738f moved axclass tutorial examples to top dir; wenzelm parents: diff changeset	18	axclass plus_semigroup < "term"
537206cc738f moved axclass tutorial examples to top dir; wenzelm parents: diff changeset	19	assoc: "(x [+] y) [+] z = x [+] (y [+] z)"
537206cc738f moved axclass tutorial examples to top dir; wenzelm parents: diff changeset	20
537206cc738f moved axclass tutorial examples to top dir; wenzelm parents: diff changeset	21	end

author	wenzelm
	Fri, 06 Oct 2000 17:35:58 +0200
changeset 10168	50be659d4222
parent 10134	537206cc738f
child 10681	ec76e17f73c5
permissions	-rw-r--r--