src/HOL/SVC_Oracle.ML
1999-09-20 paulson 1999-09-20 now uses Pattern.aeconv, not aconv, to test equality between the terms abstracted over; otherwise it is incomplete. Other changes are cosmetic
1999-08-20 wenzelm 1999-08-20 if_svc_enabled;
1999-08-19 paulson 1999-08-19 now with abstraction code previously in HOL/Tools/svc_funcs.ML
1999-08-17 wenzelm 1999-08-17 turned SVC_Oracle into a new-style theory in order to get automatic handling of its additional dependency on Tools/svc_funcs.ML;
1999-08-06 paulson 1999-08-06 svc_enabled is now declared as a function
1999-08-03 paulson 1999-08-03 biconditionals and the natural numbers
1999-08-02 paulson 1999-08-02 the SVC oracle theory