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

src/Provers/classical.ML

changeset 59119 | c90c02940964 |

parent 58963 | 26bf09b95dda |

child 59164 | ff40c53d1af9 |

equal
deleted
inserted
replaced

59118:fe7f91f85789 | 59119:c90c02940964 |
---|---|

137 instance, make_elim of Pure transforms the HOL rule injD into |
137 instance, make_elim of Pure transforms the HOL rule injD into |

138 |
138 |

139 [| inj f; f x = f y; x = y ==> PROP W |] ==> PROP W |
139 [| inj f; f x = f y; x = y ==> PROP W |] ==> PROP W |

140 |
140 |

141 Such rules can cause fast_tac to fail and blast_tac to report "PROOF |
141 Such rules can cause fast_tac to fail and blast_tac to report "PROOF |

142 FAILED"; classical_rule will strenthen this to |
142 FAILED"; classical_rule will strengthen this to |

143 |
143 |

144 [| inj f; ~ W ==> f x = f y; x = y ==> W |] ==> W |
144 [| inj f; ~ W ==> f x = f y; x = y ==> W |] ==> W |

145 *) |
145 *) |

146 |
146 |

147 fun classical_rule rule = |
147 fun classical_rule rule = |