isabelle: src/HOL/MicroJava/J/JBasis.thy@f495dba0cb07 (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
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	13	unique :: "('a \\<times> 'b) list \\<Rightarrow> bool"
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	14	"unique \\<equiv> nodups \\<circ> map fst"
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	15
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	16	end