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

src/Pure/Isar/proof.ML

changeset 19100 | 644a7a47ed02 |

parent 19078 | 97971a84f0c7 |

child 19188 | a4c82a9ff7d8 |

equal
deleted
inserted
replaced

19099:100bf66d7e85 | 19100:644a7a47ed02 |
---|---|

884 fun global_qeds txt = |
884 fun global_qeds txt = |

885 end_proof true txt |
885 end_proof true txt |

886 #> Seq.map generic_qed |
886 #> Seq.map generic_qed |

887 #> Seq.maps (fn (((_, after_qed), results), state) => |
887 #> Seq.maps (fn (((_, after_qed), results), state) => |

888 Seq.lift after_qed results (theory_of state) |
888 Seq.lift after_qed results (theory_of state) |

889 |> Seq.map (pair (context_of state))) |
889 |> Seq.map (fn thy => (ProofContext.transfer thy (context_of state), thy))) |

890 |> Seq.DETERM; (*backtracking may destroy theory!*) |
890 |> Seq.DETERM; (*backtracking may destroy theory!*) |

891 |
891 |

892 fun global_qed txt = |
892 fun global_qed txt = |

893 global_qeds txt |
893 global_qeds txt |

894 #> check_result "Failed to finish proof" |
894 #> check_result "Failed to finish proof" |