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.