| changeset 41310 | 65631ca437c9 |
| parent 41229 | d797baa3d57c |
| child 41779 | a68f503805ed |
| 41309:2e9bf718a7a1 | 41310:65631ca437c9 |
|---|---|
15 typedecl i |
15 typedecl i |
16 arities i :: "term" |
16 arities i :: "term" |
17 |
17 |
18 consts |
18 consts |
19 |
19 |
20 "0" :: "i" ("0") --{*the empty set*} |
20 zero :: "i" ("0") --{*the empty set*} |
21 Pow :: "i => i" --{*power sets*} |
21 Pow :: "i => i" --{*power sets*} |
22 Inf :: "i" --{*infinite set*} |
22 Inf :: "i" --{*infinite set*} |
23 |
23 |
24 text {*Bounded Quantifiers *} |
24 text {*Bounded Quantifiers *} |
25 consts |
25 consts |