src/HOL/Sum.ML
changeset 3842 b55686a7b22c
parent 3091 9366415b93ad
child 4089 96fba19bcbe2
     1.1 --- a/src/HOL/Sum.ML	Fri Oct 10 18:37:49 1997 +0200
     1.2 +++ b/src/HOL/Sum.ML	Fri Oct 10 19:02:28 1997 +0200
     1.3 @@ -194,7 +194,7 @@
     1.4  by (etac IntD1 1);
     1.5  qed "PartD1";
     1.6  
     1.7 -goal Sum.thy "Part A (%x.x) = A";
     1.8 +goal Sum.thy "Part A (%x. x) = A";
     1.9  by (Blast_tac 1);
    1.10  qed "Part_id";
    1.11  
    1.12 @@ -203,6 +203,6 @@
    1.13  qed "Part_Int";
    1.14  
    1.15  (*For inductive definitions*)
    1.16 -goal Sum.thy "Part (A Int {x.P x}) h = (Part A h) Int {x.P x}";
    1.17 +goal Sum.thy "Part (A Int {x. P x}) h = (Part A h) Int {x. P x}";
    1.18  by (Blast_tac 1);
    1.19  qed "Part_Collect";