| Mon, 31 Oct 2005 16:35:15 +0100 | haftmann | nth_*, fold_index refined | file | diff | annotate |
| Fri, 28 Oct 2005 22:37:57 +0200 | wenzelm | tuned; | file | diff | annotate |
| Fri, 28 Oct 2005 22:27:41 +0200 | wenzelm | * Pure/Isar: literal facts; | file | diff | annotate |
| Thu, 27 Oct 2005 13:59:06 +0200 | wenzelm | * HOL: alternative iff syntax; | file | diff | annotate |
| Thu, 27 Oct 2005 08:14:05 +0200 | haftmann | added module Pure/General/rat.ML | file | diff | annotate |
| Fri, 21 Oct 2005 18:16:57 +0200 | wenzelm | * Legacy goal package: reduced interface to the bare minimum required to keep existing proof scripts running. | file | diff | annotate |
| Wed, 19 Oct 2005 21:52:30 +0200 | wenzelm | * Theory syntax: discontinued non-Isar format and old Isar headers; | file | diff | annotate |
| Tue, 18 Oct 2005 17:59:23 +0200 | wenzelm | Simplifier.context/theory_context; | file | diff | annotate |
| Mon, 17 Oct 2005 23:10:25 +0200 | wenzelm | * Simplifier: simpset of a running simplification process contains a proof context; | file | diff | annotate |
| Mon, 17 Oct 2005 23:10:16 +0200 | wenzelm | tuned; | file | diff | annotate |
| Sat, 15 Oct 2005 00:14:30 +0200 | wenzelm | tuned; | file | diff | annotate |
| Sat, 15 Oct 2005 00:08:14 +0200 | wenzelm | * antiquotations ML_type, ML_struct; | file | diff | annotate |
| Sun, 09 Oct 2005 17:06:03 +0200 | webertj | Tactics sat and satx reimplemented, several improvements | file | diff | annotate |
| Sat, 08 Oct 2005 23:36:01 +0200 | nipkow | *** empty log message *** | file | diff | annotate |
| Fri, 07 Oct 2005 22:59:17 +0200 | wenzelm | tuned; | file | diff | annotate |
| Fri, 07 Oct 2005 22:59:15 +0200 | wenzelm | added dummy variable binding; | file | diff | annotate |
| Tue, 04 Oct 2005 16:47:39 +0200 | wenzelm | * Command 'find_theorems': support * wildcard in name: criterion. | file | diff | annotate |
| Thu, 29 Sep 2005 17:08:52 +0200 | wenzelm | pdfsetup.sty: better not rely on ifpdf.sty; | file | diff | annotate |
| Thu, 29 Sep 2005 15:50:43 +0200 | wenzelm | Isabelle2005 (October 2005); | file | diff | annotate |
| Thu, 29 Sep 2005 00:58:54 +0200 | wenzelm | tuned; | file | diff | annotate |
| Wed, 28 Sep 2005 18:50:42 +0200 | webertj | pointer to HOL/ex/SAT_Examples.thy added | file | diff | annotate |
| Wed, 28 Sep 2005 11:50:13 +0200 | wenzelm | revert 'defs' advertisement; | file | diff | annotate |
| Tue, 27 Sep 2005 17:24:27 +0200 | wenzelm | more details about incomplete 'defs'; | file | diff | annotate |
| Tue, 27 Sep 2005 11:27:07 +0200 | wenzelm | tuned; | file | diff | annotate |
| Tue, 27 Sep 2005 11:03:38 +0200 | berghofe | Added entries for code_module, code_library, and value. | file | diff | annotate |
| Sun, 25 Sep 2005 20:24:23 +0200 | wenzelm | * Hyperreal: A theory of Taylor series. | file | diff | annotate |
| Fri, 23 Sep 2005 23:28:59 +0200 | webertj | new sat tactic | file | diff | annotate |
| Fri, 23 Sep 2005 13:20:47 +0200 | wenzelm | tuned; | file | diff | annotate |
| Fri, 23 Sep 2005 10:25:55 +0200 | paulson | ATP linkup | file | diff | annotate |
| Fri, 23 Sep 2005 00:10:58 +0200 | nipkow | *** empty log message *** | file | diff | annotate |
| Thu, 22 Sep 2005 18:59:41 +0200 | huffman | HOLCF theorem naming conventions | file | diff | annotate |
| Wed, 21 Sep 2005 17:21:35 +0200 | haftmann | added AList.make, eq_fst, apr ... | file | diff | annotate |
| Wed, 21 Sep 2005 11:50:52 +0200 | wenzelm | tunes; | file | diff | annotate |
| Wed, 21 Sep 2005 00:07:32 +0200 | wenzelm | tuned; | file | diff | annotate |
| Tue, 20 Sep 2005 22:02:06 +0200 | wenzelm | tuned; | file | diff | annotate |
| Tue, 20 Sep 2005 21:48:47 +0200 | wenzelm | tuned; | file | diff | annotate |
| Tue, 20 Sep 2005 14:20:58 +0200 | wenzelm | HOL/ex/Chinese.thy; | file | diff | annotate |
| Tue, 20 Sep 2005 08:20:22 +0200 | haftmann | infix operator precedence | file | diff | annotate |
| Sat, 17 Sep 2005 18:11:17 +0200 | wenzelm | HTML.with_charset; | file | diff | annotate |
| Sat, 17 Sep 2005 12:18:00 +0200 | wenzelm | Cube: converted to Isar, use locales; | file | diff | annotate |
| Fri, 16 Sep 2005 23:55:23 +0200 | huffman | add HOLCF entries for pcpodef, cont_proc, fixrec; | file | diff | annotate |
| Fri, 16 Sep 2005 14:44:52 +0200 | ballarin | tuned | file | diff | annotate |
| Thu, 15 Sep 2005 20:27:48 +0200 | wenzelm | * Improved efficiency of the Simplifier etc.; | file | diff | annotate |
| Thu, 15 Sep 2005 20:24:53 +0200 | wenzelm | incorporated HOL/Hyperreal/CHANGES; | file | diff | annotate |
| Thu, 15 Sep 2005 17:16:53 +0200 | wenzelm | command 'thms_containing' has been discontinued in favour of 'find_theorems'; | file | diff | annotate |
| Thu, 15 Sep 2005 10:00:01 +0200 | haftmann | AList, the_* | file | diff | annotate |
| Wed, 14 Sep 2005 23:31:09 +0200 | wenzelm | tuned; | file | diff | annotate |
| Wed, 14 Sep 2005 23:15:00 +0200 | wenzelm | hide: added option '(open)'; | file | diff | annotate |
| Wed, 14 Sep 2005 23:06:02 +0200 | schirmer | ... prem19 | file | diff | annotate |
| Wed, 14 Sep 2005 22:18:55 +0200 | wenzelm | Method comm_ring for proving equalities in commutative rings. | file | diff | annotate |
| Wed, 14 Sep 2005 22:04:36 +0200 | wenzelm | HOL: method comm_ring; | file | diff | annotate |
| Tue, 13 Sep 2005 22:49:12 +0200 | wenzelm | tuned; | file | diff | annotate |
| Tue, 06 Sep 2005 16:59:50 +0200 | wenzelm | axclass: name space prefix is now "c_class" instead of just "c"; | file | diff | annotate |
| Mon, 05 Sep 2005 17:49:28 +0200 | wenzelm | tuned; | file | diff | annotate |
| Mon, 05 Sep 2005 17:38:15 +0200 | wenzelm | Markup commands 'chapter' .. 'text' support optional locale specification; | file | diff | annotate |
| Fri, 02 Sep 2005 09:50:58 +0200 | ballarin | print_locale omits facts by default | file | diff | annotate |
| Wed, 31 Aug 2005 15:46:30 +0200 | wenzelm | * Delimiters of outer tokens now produce separate LaTeX macros; | file | diff | annotate |
| Tue, 30 Aug 2005 12:47:53 +0200 | paulson | patterns in setsum and setprod | file | diff | annotate |
| Sun, 28 Aug 2005 16:06:07 +0200 | wenzelm | * ML functions legacy_bindings and use_legacy_bindings; | file | diff | annotate |
| Sun, 28 Aug 2005 16:04:50 +0200 | wenzelm | tuned; | file | diff | annotate |