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

src/Sequents/prover.ML

changeset 3948 | 3428c0a88449 |

parent 3538 | ed9de44032e0 |

child 4440 | 9ed4098074bc |

equal
deleted
inserted
replaced

3947:eb707467f8c5 | 3948:3428c0a88449 |
---|---|

27 fun (Pack(safes,unsafes)) add_unsafes ths = |
27 fun (Pack(safes,unsafes)) add_unsafes ths = |

28 Pack(safes, sort less (ths@unsafes)); |
28 Pack(safes, sort less (ths@unsafes)); |

29 |
29 |

30 |
30 |

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

32 fun forms_of_seq (Const("SeqO'",_) $ P $ u) = P :: forms_of_seq u |
32 fun forms_of_seq (Const("Sequents.SeqO'",_) $ P $ u) = P :: forms_of_seq u |

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

34 | forms_of_seq _ = []; |
34 | forms_of_seq _ = []; |

35 |
35 |

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

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

158 struct |
158 struct |

159 local open Modal_Rule |
159 local open Modal_Rule |

160 in |
160 in |

161 |
161 |

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

163 fun forms_of_seq (Const("SeqO",_) $ P $ u) = P :: forms_of_seq u |
163 fun forms_of_seq (Const("Sequents.SeqO",_) $ P $ u) = P :: forms_of_seq u |

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

165 | forms_of_seq _ = []; |
165 | forms_of_seq _ = []; |

166 |
166 |

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

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