isabelle: src/HOL/MicroJava/J/JBasis.thy@7164dc0d24d8 (annotated)

8011 d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	1	(* Title: HOL/MicroJava/J/JBasis.thy
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	2	ID: $Id$
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	3	Author: David von Oheimb
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	4	Copyright 1999 TU Muenchen
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	5
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	6	Some auxiliary definitions.
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	7	*)
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	8
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	9	JBasis = Main +
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	10
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	11	constdefs
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	12
10042 7164dc0d24d8 unsymbolized kleing parents: 8116 diff changeset	13	unique :: "('a \\<times> 'b) list => bool"
7164dc0d24d8 unsymbolized kleing parents: 8116 diff changeset	14	"unique == nodups \\<circ> map fst"
8011 d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	15
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	16	end