summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Sat, 23 Apr 2005 19:49:39 +0200 | |

changeset 15824 | 222eeb9655f3 |

parent 15823 | d1001770af17 |

child 15825 | 1576f9d3ffae |

tuned proofs;

src/Pure/Pure.thy | file | annotate | diff | comparison | revisions |

--- 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]