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

author | blanchet |

Tue, 24 Jun 2014 08:19:22 +0200 | |

changeset 57285 | a9c2272d01f6 |

parent 57284 | 886ff14f20cc |

child 57286 | 4868ec62f533 |

don't accidentally transform 'show' into 'obtains' (in general, more 'obtain's could be turned into 'have's, but this is not necessary for the correctness of the proof)

src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML | file | annotate | diff | comparison | revisions |

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Sun Jun 22 12:37:55 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Tue Jun 24 08:19:22 2014 +0200 @@ -94,8 +94,8 @@ val lfs = union (op =) lfs1 (remove (op =) l1 lfs2) val gfs = union (op =) gfs1 gfs2 in - (Prove (qs2, union (op =) fix1 fix2, l2, t, subproofs1 @ subproofs2, (lfs, gfs), meths, - comment1 ^ comment2), hopeless) + (Prove (qs2, if member (op =) qs2 Show then [] else union (op =) fix1 fix2, l2, t, + subproofs1 @ subproofs2, (lfs, gfs), meths, comment1 ^ comment2), hopeless) end val merge_slack_time = seconds 0.005