src/Pure/Pure.thy
changeset 22933 338c7890c96f
parent 21627 b822c7e61701
child 23432 cec811764a38
     1.1 --- a/src/Pure/Pure.thy	Fri May 11 00:43:46 2007 +0200
     1.2 +++ b/src/Pure/Pure.thy	Fri May 11 01:07:10 2007 +0200
     1.3 @@ -94,8 +94,11 @@
     1.4    shows "(PROP A && PROP B ==> PROP C) == (PROP A ==> PROP B ==> PROP C)"
     1.5  proof
     1.6    assume r: "PROP A && PROP B ==> PROP C"
     1.7 -  assume "PROP A" and "PROP B"
     1.8 -  show "PROP C" by (rule r) -
     1.9 +  assume ab: "PROP A" "PROP B"
    1.10 +  show "PROP C"
    1.11 +  proof (rule r)
    1.12 +    from ab show "PROP A && PROP B" .
    1.13 +  qed
    1.14  next
    1.15    assume r: "PROP A ==> PROP B ==> PROP C"
    1.16    assume conj: "PROP A && PROP B"