|
1826
|
1 |
<HTML><HEAD><TITLE>Set2g.thy</TITLE></HEAD>
|
|
|
2 |
|
|
|
3 |
<BODY>
|
|
|
4 |
<H2>Set2g.thy</H2>
|
|
|
5 |
<A HREF = "../../../../stud/oheimb/isabelle/HOL/index.html">Back</A> to the index of HOL
|
|
|
6 |
<HR>
|
|
|
7 |
|
|
|
8 |
<PRE>
|
|
|
9 |
Set2g = <A HREF = "../../../../stud/oheimb/isabelle/HOL/.Ord.html">Ord</A> +
|
|
|
10 |
|
|
|
11 |
types
|
|
|
12 |
'a set
|
|
|
13 |
consts
|
|
|
14 |
Ball :: "'a set ë ('a ë bool) ë bool"
|
|
|
15 |
syntax
|
|
|
16 |
"GBall" :: "pttrn ë 'a set ë bool ë bool" ("(3Â_Î_./ _)" 10)
|
|
|
17 |
translations
|
|
|
18 |
(* "ÂxÎA. P" == "Ball A (³x. P)"*)
|
|
|
19 |
"GBall x A P" == "Ball A (³x. P)"
|
|
|
20 |
|
|
|
21 |
(*defs
|
|
|
22 |
|
|
|
23 |
Ball_def "Ball A P Ú Âx. xÎA çè P(x)"
|
|
|
24 |
*)
|
|
|
25 |
end
|
|
|
26 |
</PRE>
|
|
|
27 |
<HR></BODY></HTML>
|