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

src/Pure/Pure.thy

changeset 15824 | 222eeb9655f3 |

parent 15803 | 42c75e0c9140 |

child 18019 | d1ff9ebb8bcb |

--- a/src/Pure/Pure.thy Sat Apr 23 19:49:26 2005 +0200 +++ b/src/Pure/Pure.thy Sat Apr 23 19:49:39 2005 +0200 @@ -18,16 +18,12 @@ lemma meta_mp: assumes major: "PROP P ==> PROP Q" and minor: "PROP P" shows "PROP Q" -proof - - show "PROP Q" by (rule major [OF minor]) -qed + by (rule major [OF minor]) lemma meta_spec: assumes major: "!!x. PROP P(x)" shows "PROP P(x)" -proof - - show "PROP P(x)" by (rule major) -qed + by (rule major) lemmas meta_allE = meta_spec [elim_format]