equal
deleted
inserted
replaced
1 (* Title: FOLP/hypsubst |
1 (* Title: FOLP/hypsubst.ML |
2 Author: Martin D Coen, Cambridge University Computer Laboratory |
2 Author: Martin D Coen, Cambridge University Computer Laboratory |
3 Copyright 1995 University of Cambridge |
3 Copyright 1995 University of Cambridge |
4 |
4 |
5 Original version of Provers/hypsubst. Cannot use new version because it |
5 Original version of Provers/hypsubst. Cannot use new version because it |
6 relies on the new simplifier! |
6 relies on the new simplifier! |