Put in minimal simpset to avoid excessive simplification,
just as in revision 1.9 of HOL/indrule.ML
<HTML><HEAD><TITLE>Set2g.thy</TITLE></HEAD>
<BODY>
<H2>Set2g.thy</H2>
<A HREF = "../../../../stud/oheimb/isabelle/HOL/index.html">Back</A> to the index of HOL
<HR>
<PRE>
Set2g = <A HREF = "../../../../stud/oheimb/isabelle/HOL/.Ord.html">Ord</A> +
types
'a set
consts
Ball :: "'a set ë ('a ë bool) ë bool"
syntax
"GBall" :: "pttrn ë 'a set ë bool ë bool" ("(3Â_Î_./ _)" 10)
translations
(* "ÂxÎA. P" == "Ball A (³x. P)"*)
"GBall x A P" == "Ball A (³x. P)"
(*defs
Ball_def "Ball A P Ú Âx. xÎA çè P(x)"
*)
end
</PRE>
<HR></BODY></HTML>