# HG changeset patch
# User wenzelm
# Date 1003170822 -7200
# Node ID b03c8a3fcc6dd250e4efb982387f008860de4c56
# Parent  d4f9de0bde28392df4eed43aba56c5d3321fcbc1
tuned;

diff -r d4f9de0bde28 -r b03c8a3fcc6d src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Mon Oct 15 20:33:05 2001 +0200
+++ b/src/HOL/Product_Type.thy	Mon Oct 15 20:33:42 2001 +0200
@@ -2,18 +2,17 @@
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
+*)
 
-Ordered Pairs and the Cartesian product type.
-The unit type.
-*)
+header {* Finite products (including unit) *}
 
 theory Product_Type = Fun
 files ("Product_Type_lemmas.ML") ("Tools/split_rule.ML"):
 
 
-(** products **)
+subsection {* Products *}
 
-(* type definition *)
+subsubsection {* Type definition *}
 
 constdefs
   Pair_Rep :: "['a, 'b] => ['a, 'b] => bool"
@@ -34,8 +33,12 @@
 syntax (HTML output)
   "*"      :: "[type, type] => type"         ("(_ \<times>/ _)" [21, 20] 20)
 
+local
 
-(* abstract constants and syntax *)
+
+subsubsection {* Abstract constants and syntax *}
+
+global
 
 consts
   fst      :: "'a * 'b => 'a"
@@ -45,8 +48,12 @@
   Pair     :: "['a, 'b] => 'a * 'b"
   Sigma    :: "['a set, 'a => 'b set] => ('a * 'b) set"
 
+local
 
-(* patterns -- extends pre-defined type "pttrn" used in abstractions *)
+text {*
+  Patterns -- extends pre-defined type @{typ pttrn} used in
+  abstractions.
+*}
 
 nonterminals
   tuple_args patterns
@@ -80,9 +87,7 @@
 print_translation {* [("Sigma", dependent_tr' ("@Sigma", "@Times"))] *}
 
 
-(* definitions *)
-
-local
+subsubsection {* Definitions *}
 
 defs
   Pair_def:     "Pair a b == Abs_Prod(Pair_Rep a b)"
@@ -93,8 +98,7 @@
   Sigma_def:    "Sigma A B == UN x:A. UN y:B(x). {(x, y)}"
 
 
-
-(** unit **)
+subsection {* Unit *}
 
 typedef unit = "{True}"
 proof
@@ -107,15 +111,15 @@
   "() == Abs_unit True"
 
 
-
-(** lemmas and tool setup **)
+subsection {* Lemmas and tool setup *}
 
 use "Product_Type_lemmas.ML"
 
 lemma pair_imageI [intro]: "(a, b) : A ==> f a b : (%(a, b). f a b) ` A"
-apply (rule_tac x = "(a,b)" in image_eqI)
-apply  auto
-done
+  apply (rule_tac x = "(a, b)" in image_eqI)
+   apply auto
+  done
+
 
 constdefs
   internal_split :: "('a => 'b => 'c) => 'a * 'b => 'c"