src/HOL/Sum.ML
changeset 1515 4ed79ebab64d
parent 1465 5d7a7e439cec
child 1760 6f41a494f3b1
     1.1 --- a/src/HOL/Sum.ML	Mon Feb 19 13:54:15 1996 +0100
     1.2 +++ b/src/HOL/Sum.ML	Mon Feb 19 18:04:41 1996 +0100
     1.3 @@ -193,6 +193,8 @@
     1.4  by (fast_tac (set_cs addSIs [PartI] addSEs [PartE]) 1);
     1.5  qed "Part_mono";
     1.6  
     1.7 +val basic_monos = basic_monos @ [Part_mono];
     1.8 +
     1.9  goalw Sum.thy [Part_def] "!!a. a : Part A h ==> a : A";
    1.10  by (etac IntD1 1);
    1.11  qed "PartD1";