tuned proof in order to avoid warning message
authorChristian Urban <urbanc@in.tum.de>
Mon Apr 02 18:12:53 2012 +0100 (2012-04-02)
changeset 47301ca743eafa1dd
parent 47300 2284a40e0f57
child 47303 2f4efbdc43ba
child 47304 a0d97d919f01
tuned proof in order to avoid warning message
src/HOL/Library/Quotient_Product.thy
     1.1 --- a/src/HOL/Library/Quotient_Product.thy	Mon Apr 02 16:07:24 2012 +0200
     1.2 +++ b/src/HOL/Library/Quotient_Product.thy	Mon Apr 02 18:12:53 2012 +0100
     1.3 @@ -85,7 +85,8 @@
     1.4  
     1.5  lemma split_rsp [quot_respect]:
     1.6    shows "((R1 ===> R2 ===> (op =)) ===> (prod_rel R1 R2) ===> (op =)) split split"
     1.7 -  by (auto intro!: fun_relI elim!: fun_relE)
     1.8 +  unfolding prod_rel_def fun_rel_def
     1.9 +  by auto
    1.10  
    1.11  lemma split_prs [quot_preserve]:
    1.12    assumes q1: "Quotient R1 Abs1 Rep1"