(* Title: isabelle/Bali/Basis.thy
ID: $Id: Basis.thy,v 1.7 1998/04/08 15:26:54 oheimb Exp $
Author: David von Oheimb
Copyright 1997 Technische Universitaet Muenchen
Definitions extending HOL as logical basis of Bali
*)
Basis = Sum + WF_Rel + Map + IntDef + Inductive +
constdefs
unique :: "('a * 'b) list => bool"
"unique t == !(x,y):set t. !(x',y'):set t. x = x' --> y = y'"
end