1995-03-03 ago added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
1995-02-27 ago Now prove_goalw_cterm calls print_sign_exn_unit, so that the rest
1994-11-03 ago Pure/goals/prepare_proof/mkresult: now smashes flexflex pairs in the final
1994-11-02 ago Modified pattern.ML to perform proper matching of Higher-Order Patterns.
1994-08-25 ago print_sign_exn: now exported, with a polymorphic type
1994-08-18 ago Pure/goals.ML: prove_goalw_cterm now does its own exception-handling, moved
1994-02-03 ago replaced eq_sg by Sign.eq_sg;
1994-01-18 ago Many other files modified as follows:
1993-10-22 ago goals/print_top,prepare_proof: now call \!print_goals_ref
1993-10-08 ago "The error/exception above ...": errorneous goal now quoted;
1993-09-16 ago Initial revision