isabelle: src/HOL/AxClasses/Semigroups.thy@7c1b59ddcd56 (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
16417 9bc16273c2d4 migrated theory headers to new format haftmann parents: 14981 diff changeset	6	theory Semigroups imports Main begin
10134 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	paulson
	Wed, 22 Nov 2006 20:08:07 +0100
changeset 21470	7c1b59ddcd56
parent 16417	9bc16273c2d4
permissions	-rw-r--r--