changeset 12633 | ad9277743664 |
parent 12338 | de0f4a63baa5 |
child 12897 | f4d10ad0ea7b |
--- a/src/HOL/Set.thy Fri Jan 04 19:28:57 2002 +0100 +++ b/src/HOL/Set.thy Fri Jan 04 19:29:30 2002 +0100 @@ -85,7 +85,7 @@ "ALL x:A. P" == "Ball A (%x. P)" "EX x:A. P" == "Bex A (%x. P)" -syntax ("" output) +syntax (output) "_setle" :: "'a set => 'a set => bool" ("op <=") "_setle" :: "'a set => 'a set => bool" ("(_/ <= _)" [50, 51] 50) "_setless" :: "'a set => 'a set => bool" ("op <")