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

src/HOL/Tools/Meson/meson.ML

changeset 46503 | 186f4cab2ba0 |

parent 46093 | 4bf24b90703c |

child 46818 | 2a28e66e2e4c |

equal
deleted
inserted
replaced

46502:3d43d4d4d071 | 46503:186f4cab2ba0 |
---|---|

754 with no contrapositives, for ordinary resolution.*) |
754 with no contrapositives, for ordinary resolution.*) |

755 |
755 |

756 (*Rules to convert the head literal into a negated assumption. If the head |
756 (*Rules to convert the head literal into a negated assumption. If the head |

757 literal is already negated, then using notEfalse instead of notEfalse' |
757 literal is already negated, then using notEfalse instead of notEfalse' |

758 prevents a double negation.*) |
758 prevents a double negation.*) |

759 val notEfalse = read_instantiate @{context} [(("R", 0), "False")] notE; |
759 val notEfalse = @{lemma "~ P ==> P ==> False" by (rule notE)}; |

760 val notEfalse' = rotate_prems 1 notEfalse; |
760 val notEfalse' = @{lemma "P ==> ~ P ==> False" by (rule notE)}; |

761 |
761 |

762 fun negated_asm_of_head th = |
762 fun negated_asm_of_head th = |

763 th RS notEfalse handle THM _ => th RS notEfalse'; |
763 th RS notEfalse handle THM _ => th RS notEfalse'; |

764 |
764 |

765 (*Converting one theorem from a disjunction to a meta-level clause*) |
765 (*Converting one theorem from a disjunction to a meta-level clause*) |