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

src/Sequents/modal.ML

changeset 69593 | 3dda49e08b9d |

parent 59582 | 0fbed69ff081 |

equal
deleted
inserted
replaced

69592:a80d8ec6c998 | 69593:3dda49e08b9d |
---|---|

24 |
24 |

25 functor Modal_ProverFun (Modal_Rule: MODAL_PROVER_RULE) : MODAL_PROVER = |
25 functor Modal_ProverFun (Modal_Rule: MODAL_PROVER_RULE) : MODAL_PROVER = |

26 struct |
26 struct |

27 |
27 |

28 (*Returns the list of all formulas in the sequent*) |
28 (*Returns the list of all formulas in the sequent*) |

29 fun forms_of_seq (Const(@{const_name SeqO'},_) $ P $ u) = P :: forms_of_seq u |
29 fun forms_of_seq (Const(\<^const_name>\<open>SeqO'\<close>,_) $ P $ u) = P :: forms_of_seq u |

30 | forms_of_seq (H $ u) = forms_of_seq u |
30 | forms_of_seq (H $ u) = forms_of_seq u |

31 | forms_of_seq _ = []; |
31 | forms_of_seq _ = []; |

32 |
32 |

33 (*Tests whether two sequences (left or right sides) could be resolved. |
33 (*Tests whether two sequences (left or right sides) could be resolved. |

34 seqp is a premise (subgoal), seqc is a conclusion of an object-rule. |
34 seqp is a premise (subgoal), seqc is a conclusion of an object-rule. |