src/FOLP/hypsubst.ML
changeset 37744 3daaf23b9ab4
parent 36692 54b64d4ad524
child 42125 a8cbb9371154
equal deleted inserted replaced
37743:0a3fa8fbcdc5 37744:3daaf23b9ab4
     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!