| Mon, 08 Oct 2001 14:30:28 +0200 | wenzelm | * added default LaTeX bindings for \<tturnstile> and \<TTurnstile>; | file | diff | annotate |
| Fri, 05 Oct 2001 23:58:17 +0200 | wenzelm | *** empty log message *** | file | diff | annotate |
| Fri, 05 Oct 2001 21:50:37 +0200 | wenzelm | *** empty log message *** | file | diff | annotate |
| Thu, 04 Oct 2001 16:07:43 +0200 | wenzelm | improved proof by cases and induction; | file | diff | annotate |
| Thu, 04 Oct 2001 11:28:30 +0200 | wenzelm | * moved induct/cases attributes to Pure, added 'print_induct_rules' command; | file | diff | annotate |
| Wed, 03 Oct 2001 20:58:27 +0200 | wenzelm | *** empty log message *** | file | diff | annotate |
| Fri, 28 Sep 2001 19:23:58 +0200 | wenzelm | *** empty log message *** | file | diff | annotate |
| Thu, 27 Sep 2001 22:30:09 +0200 | wenzelm | HOL: eliminated global items; | file | diff | annotate |
| Wed, 26 Sep 2001 22:24:55 +0200 | wenzelm | tuned; | file | diff | annotate |
| Sat, 08 Sep 2001 20:02:09 +0200 | wenzelm | * system: support Poly/ML 4.1.1 (large heaps); | file | diff | annotate |
| Tue, 04 Sep 2001 21:10:57 +0200 | wenzelm | renamed "antecedent" case to "rule_context"; | file | diff | annotate |
| Fri, 31 Aug 2001 22:46:23 +0200 | wenzelm | * Proof General keywords specification is now part of the Isabelle | file | diff | annotate |
| Thu, 09 Aug 2001 10:16:23 +0200 | oheimb | renamed addaltern to addafter, addSaltern to addSafter | file | diff | annotate |
| Wed, 08 Aug 2001 17:37:47 +0200 | wenzelm | * HOL: syntax translations now work properly with numerals and records | file | diff | annotate |
| Tue, 07 Aug 2001 22:42:22 +0200 | wenzelm | tuned; | file | diff | annotate |
| Tue, 07 Aug 2001 22:41:46 +0200 | wenzelm | tuned; | file | diff | annotate |
| Fri, 20 Jul 2001 22:02:45 +0200 | wenzelm | HOL: added "The"; | file | diff | annotate |
| Tue, 03 Jul 2001 15:40:25 +0200 | paulson | GroupTheory | file | diff | annotate |
| Tue, 05 Jun 2001 09:51:04 +0200 | nipkow | *** empty log message *** | file | diff | annotate |
| Mon, 21 May 2001 12:51:15 +0200 | paulson | ZF: division | file | diff | annotate |
| Fri, 18 May 2001 12:13:53 +0200 | nipkow | *** empty log message *** | file | diff | annotate |
| Mon, 09 Apr 2001 10:10:21 +0200 | paulson | Isar hint | file | diff | annotate |
| Fri, 23 Feb 2001 16:31:21 +0100 | oheimb | renamed addaltern to addafter, addSaltern to addSafter | file | diff | annotate |
| Wed, 21 Feb 2001 12:07:00 +0100 | oheimb | added split_conv_tac (also to claset()) as an optimization | file | diff | annotate |
| Tue, 20 Feb 2001 18:47:34 +0100 | oheimb | made split_all_tac safe introducing safe_full_simp_tac, EXISTING PROOFS MAY FAIL | file | diff | annotate |
| Thu, 15 Feb 2001 13:07:03 +0100 | oheimb | added missiong word | file | diff | annotate |
| Wed, 14 Feb 2001 23:17:53 +0100 | wenzelm | isatool install handles KDE version 1 or 2; | file | diff | annotate |
| Tue, 13 Feb 2001 22:51:08 +0100 | wenzelm | tuned; | file | diff | annotate |
| Sun, 11 Feb 2001 16:34:20 +0100 | wenzelm | more robust selection of calculational rules; | file | diff | annotate |
| Sun, 11 Feb 2001 13:26:23 +0100 | wenzelm | tuned; | file | diff | annotate |
| Sat, 10 Feb 2001 08:48:10 +0100 | ballarin | Updates to HOL/Algebra: | file | diff | annotate |
| Mon, 05 Feb 2001 14:31:49 +0100 | wenzelm | tuned; | file | diff | annotate |
| Sun, 04 Feb 2001 19:40:06 +0100 | wenzelm | * no_document ML operator temporarily disables LaTeX document | file | diff | annotate |
| Sat, 03 Feb 2001 15:20:55 +0100 | wenzelm | HOL: inductive package no longer splits induction rule aggressively, | file | diff | annotate |
| Thu, 01 Feb 2001 20:42:34 +0100 | wenzelm | * Pure: 'thms_containing' now takes actual terms as arguments; | file | diff | annotate |
| Tue, 30 Jan 2001 14:21:50 +0100 | wenzelm | tuned; | file | diff | annotate |
| Wed, 24 Jan 2001 21:01:47 +0100 | wenzelm | * Document preparation: renamed standard symbols \<ll> to \<lless> and | file | diff | annotate |
| Tue, 23 Jan 2001 18:05:53 +0100 | wenzelm | added HOL-Unix example; | file | diff | annotate |
| 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 |