isabelle: src/Pure/class.ML@6a7a19517ba8 (annotated)

16524 6a7a19517ba8 (initial commit) haftmann parents: diff changeset	1	(* Title: Pure/class.ML
6a7a19517ba8 (initial commit) haftmann parents: diff changeset	2	ID: $Id$
6a7a19517ba8 (initial commit) haftmann parents: diff changeset	3	Author: Florian Haftmann, TU Muenchen
6a7a19517ba8 (initial commit) haftmann parents: diff changeset	4
6a7a19517ba8 (initial commit) haftmann parents: diff changeset	5	Haskell98-like type classes, simulated by locales
6a7a19517ba8 (initial commit) haftmann parents: diff changeset	6	*)
6a7a19517ba8 (initial commit) haftmann parents: diff changeset	7
6a7a19517ba8 (initial commit) haftmann parents: diff changeset	8	(!!! for now, only experimental scratch code !!!)
6a7a19517ba8 (initial commit) haftmann parents: diff changeset	9
6a7a19517ba8 (initial commit) haftmann parents: diff changeset	10	signature CLASS =
6a7a19517ba8 (initial commit) haftmann parents: diff changeset	11	sig
6a7a19517ba8 (initial commit) haftmann parents: diff changeset	12
6a7a19517ba8 (initial commit) haftmann parents: diff changeset	13	end
6a7a19517ba8 (initial commit) haftmann parents: diff changeset	14
6a7a19517ba8 (initial commit) haftmann parents: diff changeset	15	structure Class : CLASS =
6a7a19517ba8 (initial commit) haftmann parents: diff changeset	16	struct
6a7a19517ba8 (initial commit) haftmann parents: diff changeset	17
6a7a19517ba8 (initial commit) haftmann parents: diff changeset	18	end;