# HG changeset patch # User wenzelm # Date 850495356 -3600 # Node ID d1f0505fc60273ce1f0e26111c774b61173eb59f # Parent 1b37895b607aa8e7e2816347a546b13be06bd44f added set inclusion symbol syntax; diff -r 1b37895b607a -r d1f0505fc602 src/HOL/Set.thy --- a/src/HOL/Set.thy Fri Dec 13 17:38:56 1996 +0100 +++ b/src/HOL/Set.thy Fri Dec 13 17:42:36 1996 +0100 @@ -84,8 +84,13 @@ "ALL x:A. P" => "Ball A (%x. P)" "EX x:A. P" => "Bex A (%x. P)" +syntax ("" output) + "_setle" :: ['a set, 'a set] => bool ("(_/ <= _)" [50, 51] 50) + "_setle" :: ['a set, 'a set] => bool ("op <=") syntax (symbols) + "_setle" :: ['a set, 'a set] => bool ("(_/ \\ _)" [50, 51] 50) + "_setle" :: ['a set, 'a set] => bool ("op \\") "op Int" :: ['a set, 'a set] => 'a set (infixl "\\" 70) "op Un" :: ['a set, 'a set] => 'a set (infixl "\\" 65) "op :" :: ['a, 'a set] => bool ("(_/ \\ _)" [50, 51] 50) @@ -140,8 +145,6 @@ inj_onto_def "inj_onto f A == ! x:A. ! y:A. f(x)=f(y) --> x=y" surj_def "surj(f) == ! y. ? x. y=f(x)" -(* start 8bit 1 *) -(* end 8bit 1 *) end @@ -150,6 +153,13 @@ local +(* Set inclusion *) + +fun le_tr' (*op <=*) (Type ("fun", (Type ("set", _) :: _))) ts = + list_comb (Syntax.const "_setle", ts) + | le_tr' (*op <=*) _ _ = raise Match; + + (* Translates between { e | x1..xn. P} and {u. ? x1..xn. u=e & P} *) (* {y. ? x1..xn. y = e & P} is only translated if [0..n] subset bvs(e) *) @@ -182,6 +192,7 @@ val parse_translation = [("@SetCompr", setcompr_tr)]; val print_translation = [("Collect", setcompr_tr')]; +val typed_print_translation = [("op <=", le_tr')]; val print_ast_translation = map HOL.alt_ast_tr' [("@Ball", "*Ball"), ("@Bex", "*Bex")];