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

author | wenzelm |

Thu, 10 Oct 2019 15:00:36 +0200 | |

changeset 71014 | 7000868c6098 |

parent 71013 | c6f2a73987cd |

child 71015 | 3c215bdf4ab6 |

clarified modules;

src/Pure/proofterm.ML | file | annotate | diff | comparison | revisions | |

src/Pure/thm.ML | file | annotate | diff | comparison | revisions |

--- a/src/Pure/proofterm.ML Thu Oct 10 14:55:26 2019 +0200 +++ b/src/Pure/proofterm.ML Thu Oct 10 15:00:36 2019 +0200 @@ -103,6 +103,7 @@ val term_of_proof: proof -> term (*proof terms for specific inference rules*) + val trivial_proof: proof val implies_intr_proof: term -> proof -> proof val implies_intr_proof': term -> proof -> proof val forall_intr_proof: string * term -> typ option -> proof -> proof @@ -845,6 +846,11 @@ (** inference rules **) +(* trivial implication *) + +val trivial_proof = AbsP ("H", NONE, PBound 0); + + (* implication introduction *) fun gen_implies_intr_proof f h prf =

--- a/src/Pure/thm.ML Thu Oct 10 14:55:26 2019 +0200 +++ b/src/Pure/thm.ML Thu Oct 10 15:00:36 2019 +0200 @@ -1631,7 +1631,7 @@ if T <> propT then raise THM ("trivial: the term must have type prop", 0, []) else - Thm (deriv_rule0 (fn () => Proofterm.AbsP ("H", NONE, Proofterm.PBound 0)), + Thm (deriv_rule0 (fn () => Proofterm.trivial_proof), {cert = cert, tags = [], maxidx = maxidx,