| Sat, 20 Jan 2001 00:01:40 +0100 | wenzelm | *** empty log message *** | file | diff | annotate |
| Tue, 16 Jan 2001 00:37:41 +0100 | wenzelm | * HOL/datatype: induction rule for arbitrarily branching datatypes is | file | diff | annotate |
| Thu, 11 Jan 2001 12:49:48 +0100 | nipkow | *** empty log message *** | file | diff | annotate |
| Wed, 10 Jan 2001 20:21:11 +0100 | wenzelm | isatool unsymbolize; | file | diff | annotate |
| Wed, 10 Jan 2001 20:18:55 +0100 | wenzelm | tuned; | file | diff | annotate |
| Wed, 10 Jan 2001 13:30:25 +0100 | nipkow | *** empty log message *** | file | diff | annotate |
| Sat, 06 Jan 2001 10:36:19 +0100 | nipkow | *** empty log message *** | file | diff | annotate |
| Fri, 05 Jan 2001 18:31:48 +0100 | nipkow | *** empty log message *** | file | diff | annotate |
| Wed, 03 Jan 2001 21:21:28 +0100 | wenzelm | * Isar/HOL: added 'recdef_tc' command; | file | diff | annotate |
| Mon, 01 Jan 2001 11:50:31 +0100 | paulson | Hyperreal | file | diff | annotate |
| Fri, 22 Dec 2000 18:20:55 +0100 | wenzelm | tuned; | file | diff | annotate |
| Wed, 13 Dec 2000 16:21:40 +0100 | wenzelm | * print modes "brackets" and "no_brackets" control output of nested => | file | diff | annotate |
| Thu, 07 Dec 2000 22:35:25 +0100 | wenzelm | tuned; | file | diff | annotate |
| Wed, 06 Dec 2000 13:59:42 +0100 | bauerg | HOL/Real: "rinv" and "hrinv" replaced by overloaded "inverse" function; | file | diff | annotate |
| Thu, 30 Nov 2000 20:18:00 +0100 | wenzelm | tuned; | file | diff | annotate |
| Thu, 30 Nov 2000 20:03:39 +0100 | wenzelm | misc; | file | diff | annotate |
| Thu, 23 Nov 2000 21:29:35 +0100 | wenzelm | * HOL: syntax or "abs"; | file | diff | annotate |
| Thu, 16 Nov 2000 10:44:59 +0100 | paulson | CTT | file | diff | annotate |
| Mon, 13 Nov 2000 08:53:57 +0100 | nipkow | Removed > and >= | file | diff | annotate |
| Fri, 10 Nov 2000 19:20:17 +0100 | wenzelm | * added overloaded operations "inverse" and "divide" (infix "/"); | file | diff | annotate |
| Fri, 10 Nov 2000 16:31:28 +0100 | nipkow | > etc | file | diff | annotate |
| Wed, 08 Nov 2000 17:46:24 +0100 | nipkow | subgoals | file | diff | annotate |
| Mon, 06 Nov 2000 22:48:42 +0100 | wenzelm | * Isar/HOL: method 'induct' now handles non-atomic goals; as a | file | diff | annotate |
| Sat, 04 Nov 2000 18:39:44 +0100 | wenzelm | misc stuff; | file | diff | annotate |
| Wed, 25 Oct 2000 18:36:01 +0200 | wenzelm | added HOL/Library/List_Prefix; | file | diff | annotate |
| Tue, 24 Oct 2000 23:38:56 +0200 | wenzelm | * support sub/super scripts (for single symbols only), input syntax is | file | diff | annotate |
| Mon, 23 Oct 2000 22:07:08 +0200 | wenzelm | * HOL: default proof step now includes 'intro_classes'; | file | diff | annotate |
| Mon, 23 Oct 2000 10:20:55 +0200 | paulson | contrapos | file | diff | annotate |
| Wed, 18 Oct 2000 23:24:39 +0200 | wenzelm | * HOL/Library: a collection of generic theories to be used together | file | diff | annotate |
| Mon, 16 Oct 2000 10:59:35 +0200 | nipkow | *** empty log message *** | file | diff | annotate |