# 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"))];
+