added proper subset symbols syntax;
authorwenzelm
Tue Feb 25 16:57:25 1997 +0100 (1997-02-25)
changeset 26849781d63ef063
parent 2683 be7b439baef2
child 2685 8b3a214125f7
added proper subset symbols syntax;
src/HOL/Set.thy
     1.1 --- a/src/HOL/Set.thy	Tue Feb 25 15:12:49 1997 +0100
     1.2 +++ b/src/HOL/Set.thy	Tue Feb 25 16:57:25 1997 +0100
     1.3 @@ -87,10 +87,14 @@
     1.4  syntax ("" output)
     1.5    "_setle"      :: ['a set, 'a set] => bool           ("(_/ <= _)" [50, 51] 50)
     1.6    "_setle"      :: ['a set, 'a set] => bool           ("op <=")
     1.7 +  "_setless"    :: ['a set, 'a set] => bool           ("(_/ < _)" [50, 51] 50)
     1.8 +  "_setless"    :: ['a set, 'a set] => bool           ("op <")
     1.9  
    1.10  syntax (symbols)
    1.11    "_setle"      :: ['a set, 'a set] => bool           ("(_/ \\<subseteq> _)" [50, 51] 50)
    1.12    "_setle"      :: ['a set, 'a set] => bool           ("op \\<subseteq>")
    1.13 +  "_setless"    :: ['a set, 'a set] => bool           ("(_/ \\<subset> _)" [50, 51] 50)
    1.14 +  "_setless"    :: ['a set, 'a set] => bool           ("op \\<subset>")
    1.15    "op Int"      :: ['a set, 'a set] => 'a set         (infixl "\\<inter>" 70)
    1.16    "op Un"       :: ['a set, 'a set] => 'a set         (infixl "\\<union>" 65)
    1.17    "op :"        :: ['a, 'a set] => bool               ("(_/ \\<in> _)" [50, 51] 50)
    1.18 @@ -112,6 +116,7 @@
    1.19  
    1.20  translations
    1.21    "op \\<subseteq>" => "op <="
    1.22 +  "op \\<subset>" => "op <"
    1.23  
    1.24  
    1.25  
    1.26 @@ -161,6 +166,10 @@
    1.27        list_comb (Syntax.const "_setle", ts)
    1.28    | le_tr' (*op <=*) _ _ = raise Match;
    1.29  
    1.30 +fun less_tr' (*op <*) (Type ("fun", (Type ("set", _) :: _))) ts =
    1.31 +      list_comb (Syntax.const "_setless", ts)
    1.32 +  | less_tr' (*op <*) _ _ = raise Match;
    1.33 +
    1.34  
    1.35  (* Translates between { e | x1..xn. P} and {u. ? x1..xn. u=e & P}      *)
    1.36  (* {y. ? x1..xn. y = e & P} is only translated if [0..n] subset bvs(e) *)
    1.37 @@ -194,7 +203,7 @@
    1.38  
    1.39  val parse_translation = [("@SetCompr", setcompr_tr)];
    1.40  val print_translation = [("Collect", setcompr_tr')];
    1.41 -val typed_print_translation = [("op <=", le_tr')];
    1.42 +val typed_print_translation = [("op <=", le_tr'), ("op <", less_tr')];
    1.43  val print_ast_translation =
    1.44    map HOL.alt_ast_tr' [("@Ball", "*Ball"), ("@Bex", "*Bex")];
    1.45