isabelle: src/HOL/AxClasses/Tutorial/Semigroups.thy@8e9a8ede2f11 (annotated)

1247 18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	1	(* Title: HOL/AxClasses/Tutorial/Semigroups.thy
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	2	ID: $Id$
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	3	Author: Markus Wenzel, TU Muenchen
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	4	*)
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	5
10007 64bf7da1994a isar-strip-terminators; wenzelm parents: 8920 diff changeset	6	theory Semigroups = Main:
1247 18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	7
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	8	consts
10007 64bf7da1994a isar-strip-terminators; wenzelm parents: 8920 diff changeset	9	times :: "'a => 'a => 'a" (infixl "[*]" 70)
1247 18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	10	axclass
8920 af5e09b6c208 new Isar version; wenzelm parents: 1573 diff changeset	11	semigroup < "term"
10007 64bf7da1994a isar-strip-terminators; wenzelm parents: 8920 diff changeset	12	assoc: "(x [] y) [] z = x [] (y [] z)"
1247 18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	13
8920 af5e09b6c208 new Isar version; wenzelm parents: 1573 diff changeset	14	consts
10007 64bf7da1994a isar-strip-terminators; wenzelm parents: 8920 diff changeset	15	plus :: "'a => 'a => 'a" (infixl "[+]" 70)
1247 18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	16	axclass
8920 af5e09b6c208 new Isar version; wenzelm parents: 1573 diff changeset	17	plus_semigroup < "term"
10007 64bf7da1994a isar-strip-terminators; wenzelm parents: 8920 diff changeset	18	assoc: "(x [+] y) [+] z = x [+] (y [+] z)"
1247 18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	19
10007 64bf7da1994a isar-strip-terminators; wenzelm parents: 8920 diff changeset	20	end

author	wenzelm
	Tue, 03 Oct 2000 01:15:11 +0200
changeset 10132	8e9a8ede2f11
parent 10007	64bf7da1994a
permissions	-rw-r--r--