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