# HG changeset patch # User nipkow # Date 828550924 -7200 # Node ID e18416e3e1d48ded675b0aad677a93ac9bcb8531 # Parent aa09de258498c980eb2a5818f95132f553f5565d Introduced Times and SIGMA. diff -r aa09de258498 -r e18416e3e1d4 src/HOL/Prod.thy --- a/src/HOL/Prod.thy Wed Apr 03 18:27:23 1996 +0200 +++ b/src/HOL/Prod.thy Wed Apr 03 19:02:04 1996 +0200 @@ -42,6 +42,11 @@ "" :: pttrn => pttrns ("_") "@pttrns" :: [pttrn,pttrns] => pttrns ("_,/_") + "@Sigma" :: "[idt,'a set,'b set] => ('a * 'b)set" + ("(3SIGMA _:_./ _)" 10) + "@Times" :: "['a set, 'a => 'b set] => ('a * 'b) set" + ("_ Times _" [81,80] 80) + translations "(x, y, z)" == "(x, (y, z))" "(x, y)" == "Pair x y" @@ -49,6 +54,9 @@ "%(x,y,zs).b" == "split(%x (y,zs).b)" "%(x,y).b" == "split(%x y.b)" + "SIGMA x:A. B" => "Sigma A (%x.B)" + "A Times B" => "Sigma A (_K B)" + defs Pair_def "Pair a b == Abs_Prod(Pair_Rep a b)" fst_def "fst(p) == @a. ? b. p = (a, b)" @@ -72,3 +80,8 @@ (* end 8bit 1 *) end + +ML + +val print_translation = [("Sigma", dependent_tr' ("@Sigma", "@Times"))]; +