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

src/Sequents/prover.ML

changeset 29269 | 5c25a2012975 |

parent 26928 | ca87aff1ad2d |

child 32091 | 30e2ffbba718 |

--- a/src/Sequents/prover.ML Wed Dec 31 00:08:14 2008 +0100 +++ b/src/Sequents/prover.ML Wed Dec 31 15:30:10 2008 +0100 @@ -1,9 +1,8 @@ -(* Title: Sequents/prover - ID: $Id$ +(* Title: Sequents/prover.ML Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1992 University of Cambridge -Simple classical reasoner for the sequent calculus, based on "theorem packs" +Simple classical reasoner for the sequent calculus, based on "theorem packs". *) @@ -65,7 +64,7 @@ -- checks that each concl formula looks like some subgoal formula. It SHOULD check order as well, using recursion rather than forall/exists*) fun could_res (seqp,seqc) = - forall (fn Qc => exists (fn Qp => could_unify (Qp,Qc)) + forall (fn Qc => exists (fn Qp => Term.could_unify (Qp,Qc)) (forms_of_seq seqp)) (forms_of_seq seqc); @@ -78,7 +77,7 @@ could_res (leftp,leftc) andalso could_res (rightp,rightc) | (_ $ Abs(_,_,leftp) $ rightp, _ $ Abs(_,_,leftc) $ rightc) => - could_res (leftp,leftc) andalso could_unify (rightp,rightc) + could_res (leftp,leftc) andalso Term.could_unify (rightp,rightc) | _ => false;