src/HOL/Product_Type.thy
changeset 11966 8fe2ee787608
parent 11838 02d75712061d
child 12114 a8e860c86252
     1.1 --- a/src/HOL/Product_Type.thy	Sat Oct 27 23:15:52 2001 +0200
     1.2 +++ b/src/HOL/Product_Type.thy	Sat Oct 27 23:16:15 2001 +0200
     1.3 @@ -147,7 +147,7 @@
     1.4    Sigma_def:    "Sigma A B == UN x:A. UN y:B(x). {(x, y)}"
     1.5  
     1.6  
     1.7 -subsubsection {* Lemmas and tool setup *}
     1.8 +subsubsection {* Lemmas and proof tool setup *}
     1.9  
    1.10  lemma ProdI: "Pair_Rep a b : Prod"
    1.11    by (unfold Prod_def) blast