equal
deleted
inserted
replaced
27 struct |
27 struct |
28 local open Modal_Rule |
28 local open Modal_Rule |
29 in |
29 in |
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(@{const_name 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. |