summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/Pure/Pure.thy

changeset 22933 | 338c7890c96f |

parent 21627 | b822c7e61701 |

child 23432 | cec811764a38 |

--- a/src/Pure/Pure.thy Fri May 11 00:43:46 2007 +0200 +++ b/src/Pure/Pure.thy Fri May 11 01:07:10 2007 +0200 @@ -94,8 +94,11 @@ shows "(PROP A && PROP B ==> PROP C) == (PROP A ==> PROP B ==> PROP C)" proof assume r: "PROP A && PROP B ==> PROP C" - assume "PROP A" and "PROP B" - show "PROP C" by (rule r) - + assume ab: "PROP A" "PROP B" + show "PROP C" + proof (rule r) + from ab show "PROP A && PROP B" . + qed next assume r: "PROP A ==> PROP B ==> PROP C" assume conj: "PROP A && PROP B"