src/HOL/Univ.ML
changeset 5278 a903b66822e2
parent 5191 8ceaa19f7717
child 5316 7a8975451a89
     1.1 --- a/src/HOL/Univ.ML	Thu Aug 06 15:47:26 1998 +0200
     1.2 +++ b/src/HOL/Univ.ML	Thu Aug 06 15:48:13 1998 +0200
     1.3 @@ -553,8 +553,7 @@
     1.4  val dprod_subset_Sigma = [dprod_mono, dprod_Sigma] MRS subset_trans |>standard;
     1.5  
     1.6  (*Dependent version*)
     1.7 -Goal
     1.8 -    "(Sigma A B <**> Sigma C D) <= Sigma (A<*>C) (Split(%x y. B(x)<*>D(y)))";
     1.9 +Goal "(Sigma A B <**> Sigma C D) <= Sigma (A<*>C) (Split(%x y. B(x)<*>D(y)))";
    1.10  by Safe_tac;
    1.11  by (stac Split 1);
    1.12  by (Blast_tac 1);