src/Provers/trancl.ML
2007-02-07 berghofe 2007-02-07 "prove" function now instantiates relation variable in order to avoid problems with higher-order unification. This allows relations to be encoded as binary predicates.
2005-03-04 skalberg 2005-03-04 Removed practically all references to Library.foldr.
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2004-08-02 ballarin 2004-08-02 Documentation added/improved.
2004-07-27 ballarin 2004-07-27 *** empty log message ***
2004-07-26 ballarin 2004-07-26 New prover for transitive and reflexive-transitive closure of relations. - Code in Provers/trancl.ML - HOL: Simplifier set up to use it as solver