| Mon, 22 Oct 2001 11:54:22 +0200 | paulson | Numerals now work for the integers: the binary numerals for 0 and 1 rewrite | file | diff | annotate |
| Mon, 08 Oct 2001 12:27:19 +0200 | wenzelm | replace 0r/1r by 0/1; | file | diff | annotate |
| Mon, 20 Sep 1999 10:40:08 +0200 | paulson | now uses Pattern.aeconv, not aconv, to test equality between the terms | file | diff | annotate |
| Fri, 20 Aug 1999 15:41:53 +0200 | wenzelm | if_svc_enabled; | file | diff | annotate |
| Thu, 19 Aug 1999 15:12:51 +0200 | paulson | now with abstraction code previously in HOL/Tools/svc_funcs.ML | file | diff | annotate |
| Tue, 17 Aug 1999 22:11:05 +0200 | wenzelm | turned SVC_Oracle into a new-style theory in order to get automatic | file | diff | annotate |
| Fri, 06 Aug 1999 17:28:45 +0200 | paulson | svc_enabled is now declared as a function | file | diff | annotate |
| Tue, 03 Aug 1999 13:08:58 +0200 | paulson | biconditionals and the natural numbers | file | diff | annotate |
| Mon, 02 Aug 1999 11:26:43 +0200 | paulson | the SVC oracle theory | file | diff | annotate |