instance int :: ordered_ring moved to Ring_and_Field_Example, because
it changes the way that int expressions get simplified, violating
the strict library principle (cf. README.html);
(* Title: HOL/MicroJava/J/JBasis.thy
ID: $Id$
Author: David von Oheimb
Copyright 1999 TU Muenchen
Some auxiliary definitions.
*)
JBasis = Main +
constdefs
unique :: "('a \\<times> 'b) list => bool"
"unique == nodups \\<circ> map fst"
end