isabelle: src/HOL/AxClasses/Semigroups.thy@1381e90c2694 (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
12338 de0f4a63baa5 renamed class "term" to "type" (actually "HOL.type"); wenzelm parents: 10681 diff changeset	11	axclass semigroup < type
10134 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
12338 de0f4a63baa5 renamed class "term" to "type" (actually "HOL.type"); wenzelm parents: 10681 diff changeset	18	axclass plus_semigroup < type
10134 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
	Tue, 31 May 2005 11:53:14 +0200
changeset 16123	1381e90c2694
parent 14981	e73f8140af78
child 16417	9bc16273c2d4
permissions	-rw-r--r--