Introduced Times and SIGMA.
authornipkow
Wed Apr 03 19:02:04 1996 +0200 (1996-04-03)
changeset 1636e18416e3e1d4
parent 1635 aa09de258498
child 1637 b8a8ae2e5de1
Introduced Times and SIGMA.
src/HOL/Prod.thy
     1.1 --- a/src/HOL/Prod.thy	Wed Apr 03 18:27:23 1996 +0200
     1.2 +++ b/src/HOL/Prod.thy	Wed Apr 03 19:02:04 1996 +0200
     1.3 @@ -42,6 +42,11 @@
     1.4    ""        ::  pttrn         => pttrns             ("_")
     1.5    "@pttrns" :: [pttrn,pttrns] => pttrns             ("_,/_")
     1.6  
     1.7 +  "@Sigma"  :: "[idt,'a set,'b set] => ('a * 'b)set"
     1.8 +               ("(3SIGMA _:_./ _)" 10)
     1.9 +  "@Times"  :: "['a set, 'a => 'b set] => ('a * 'b) set"
    1.10 +               ("_ Times _" [81,80] 80)
    1.11 +
    1.12  translations
    1.13    "(x, y, z)"   == "(x, (y, z))"
    1.14    "(x, y)"      == "Pair x y"
    1.15 @@ -49,6 +54,9 @@
    1.16    "%(x,y,zs).b"   == "split(%x (y,zs).b)"
    1.17    "%(x,y).b"      == "split(%x y.b)"
    1.18  
    1.19 +  "SIGMA x:A. B"  =>  "Sigma A (%x.B)"
    1.20 +  "A Times B"     =>  "Sigma A (_K B)"
    1.21 +
    1.22  defs
    1.23    Pair_def      "Pair a b == Abs_Prod(Pair_Rep a b)"
    1.24    fst_def       "fst(p) == @a. ? b. p = (a, b)"
    1.25 @@ -72,3 +80,8 @@
    1.26  (* end 8bit 1 *)
    1.27  
    1.28  end
    1.29 +
    1.30 +ML
    1.31 +
    1.32 +val print_translation = [("Sigma", dependent_tr' ("@Sigma", "@Times"))];
    1.33 +