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

src/Sequents/modal.ML

changeset 29269 | 5c25a2012975 |

parent 24584 | 01e83ffa6c54 |

child 32960 | 69916a850301 |

--- a/src/Sequents/modal.ML Wed Dec 31 00:08:14 2008 +0100 +++ b/src/Sequents/modal.ML Wed Dec 31 15:30:10 2008 +0100 @@ -1,9 +1,8 @@ (* Title: Sequents/modal.ML - ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1992 University of Cambridge -Simple modal reasoner +Simple modal reasoner. *) @@ -39,7 +38,7 @@ Assumes each formula in seqc is surrounded by sequence variables -- checks that each concl formula looks like some subgoal formula.*) 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);