equal
deleted
inserted
replaced
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. |