src/HOL/Product_Type.thy
changeset 11451 8abfb4f7bd02
parent 11425 4988fd27d6e6
child 11493 f3ff2549cdc8
     1.1 --- a/src/HOL/Product_Type.thy	Tue Jul 24 11:25:54 2001 +0200
     1.2 +++ b/src/HOL/Product_Type.thy	Wed Jul 25 13:13:01 2001 +0200
     1.3 @@ -30,9 +30,9 @@
     1.4  qed
     1.5  
     1.6  syntax (symbols)
     1.7 -  "*"      :: "[type, type] => type"         ("(_ \<times>/ _)" [21, 20] 20)
     1.8 +  "*"      :: "[type, type] => type"         ("(_ \\<times>/ _)" [21, 20] 20)
     1.9  syntax (HTML output)
    1.10 -  "*"      :: "[type, type] => type"         ("(_ \<times>/ _)" [21, 20] 20)
    1.11 +  "*"      :: "[type, type] => type"         ("(_ \\<times>/ _)" [21, 20] 20)
    1.12  
    1.13  
    1.14  (* abstract constants and syntax *)
    1.15 @@ -74,8 +74,8 @@
    1.16    "A <*> B"      => "Sigma A (_K B)"
    1.17  
    1.18  syntax (symbols)
    1.19 -  "@Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set"  ("(3\<Sigma> _\<in>_./ _)"   10)
    1.20 -  "@Times" :: "['a set,  'a => 'b set] => ('a * 'b) set"  ("_ \<times> _" [81, 80] 80)
    1.21 +  "@Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set"  ("(3\\<Sigma> _\\<in>_./ _)"   10)
    1.22 +  "@Times" :: "['a set,  'a => 'b set] => ('a * 'b) set"  ("_ \\<times> _" [81, 80] 80)
    1.23  
    1.24  print_translation {* [("Sigma", dependent_tr' ("@Sigma", "@Times"))] *}
    1.25  
    1.26 @@ -86,8 +86,8 @@
    1.27  
    1.28  defs
    1.29    Pair_def:     "Pair a b == Abs_Prod(Pair_Rep a b)"
    1.30 -  fst_def:      "fst p == SOME a. EX b. p = (a, b)"
    1.31 -  snd_def:      "snd p == SOME b. EX a. p = (a, b)"
    1.32 +  fst_def:      "fst p == THE a. EX b. p = (a, b)"
    1.33 +  snd_def:      "snd p == THE b. EX a. p = (a, b)"
    1.34    split_def:    "split == (%c p. c (fst p) (snd p))"
    1.35    prod_fun_def: "prod_fun f g == split(%x y.(f(x), g(y)))"
    1.36    Sigma_def:    "Sigma A B == UN x:A. UN y:B(x). {(x, y)}"