| Mon, 24 Jan 2005 18:07:10 +0100 | berghofe | Replaced xstring by thmref. | file | diff | annotate |
| Sun, 11 Jul 2004 20:33:22 +0200 | wenzelm | local_cla/simpset_of; | file | diff | annotate |
| Mon, 21 Jun 2004 10:25:57 +0200 | kleing | Merged in license change from Isabelle2004 | file | diff | annotate |
| Fri, 17 Oct 2003 11:04:36 +0200 | paulson | Prevent recdef from looping when the inductio rule is simplified | file | diff | annotate |
| Tue, 12 Feb 2002 20:28:27 +0100 | wenzelm | got rid of explicit marginal comments (now stripped earlier from input); | file | diff | annotate |
| Tue, 15 Jan 2002 00:08:51 +0100 | wenzelm | removed case_numbers (already covered by default); | file | diff | annotate |
| Fri, 11 Jan 2002 00:28:24 +0100 | wenzelm | clarified IsarThy.apply_theorems_i; | file | diff | annotate |
| Thu, 10 Jan 2002 01:11:43 +0100 | wenzelm | simplified IsarThy.theorem_i; | file | diff | annotate |
| Mon, 10 Dec 2001 15:34:15 +0100 | berghofe | Recursive equations to be used for code generation are now registered | file | diff | annotate |
| Wed, 05 Dec 2001 03:06:05 +0100 | wenzelm | tuned; | file | diff | annotate |
| Wed, 28 Nov 2001 00:46:26 +0100 | wenzelm | theory data: removed obsolete finish method; | file | diff | annotate |
| Thu, 08 Nov 2001 23:59:37 +0100 | wenzelm | theory data: finish method; | file | diff | annotate |
| Sun, 04 Nov 2001 20:56:59 +0100 | wenzelm | IsarThy.theorem_i (None, []); | file | diff | annotate |
| Wed, 31 Oct 2001 21:59:07 +0100 | wenzelm | IsarThy.theorem_i: no locale; | file | diff | annotate |
| Sat, 13 Oct 2001 20:31:34 +0200 | wenzelm | IsarThy.theorem_i Drule.internalK; | file | diff | annotate |
| Fri, 28 Sep 2001 19:21:26 +0200 | wenzelm | permissive option; | file | diff | annotate |
| Wed, 03 Jan 2001 21:25:23 +0100 | wenzelm | added recdef_tc(_i); | file | diff | annotate |
| Thu, 19 Oct 2000 01:47:50 +0200 | wenzelm | added tcs_of; | file | diff | annotate |
| Tue, 19 Sep 2000 23:52:00 +0200 | wenzelm | tuned; | file | diff | annotate |
| Fri, 15 Sep 2000 20:22:36 +0200 | wenzelm | added "congs" keyword; | file | diff | annotate |
| Fri, 15 Sep 2000 19:34:28 +0200 | wenzelm | "hints" made keyword again; | file | diff | annotate |
| Wed, 13 Sep 2000 22:28:50 +0200 | wenzelm | tuned recdef hints; | file | diff | annotate |
| Thu, 07 Sep 2000 20:51:07 +0200 | wenzelm | tuned msg; | file | diff | annotate |
| Wed, 06 Sep 2000 19:01:37 +0200 | wenzelm | make SML/NJ happy; | file | diff | annotate |
| Wed, 06 Sep 2000 16:54:12 +0200 | wenzelm | tuned; | file | diff | annotate |
| Tue, 05 Sep 2000 18:49:26 +0200 | wenzelm | recdef hints (attributes and modifiers); | file | diff | annotate |
| Fri, 18 Aug 2000 18:06:10 +0200 | wenzelm | removed obsolete add_recdef_x; | file | diff | annotate |
| Thu, 17 Aug 2000 18:31:12 +0200 | nipkow | installed recdef congs data | file | diff | annotate |
| Tue, 18 Apr 2000 14:54:08 +0200 | wenzelm | removed obsolete "simpset" keyword; | file | diff | annotate |
| Thu, 13 Apr 2000 17:49:42 +0200 | wenzelm | outer syntax: no simps; | file | diff | annotate |
| Sat, 01 Apr 2000 20:21:39 +0200 | wenzelm | recdef: admit names/atts; | file | diff | annotate |
| Thu, 30 Mar 2000 19:47:17 +0200 | nipkow | If all termination conditions are proved automatically, | file | diff | annotate |
| Wed, 15 Mar 2000 23:40:59 +0100 | berghofe | get_recdef now returns None instead of raising ERROR. | file | diff | annotate |
| Mon, 13 Mar 2000 13:18:59 +0100 | wenzelm | adapted to new PureThy.add_thms etc.; | file | diff | annotate |
| Fri, 08 Oct 1999 15:08:23 +0200 | wenzelm | return stored thms with proper naming in derivation; | file | diff | annotate |
| Wed, 18 Aug 1999 18:44:20 +0200 | paulson | from Konrad: support for schematic definitions | file | diff | annotate |
| Mon, 28 Jun 1999 21:48:36 +0200 | wenzelm | cond_extern_table; | file | diff | annotate |
| Tue, 25 May 1999 20:24:10 +0200 | wenzelm | formal comments (still dummy); | file | diff | annotate |
| Mon, 24 May 1999 21:57:13 +0200 | wenzelm | outer syntax keyword classification; | file | diff | annotate |
| Tue, 04 May 1999 16:18:16 +0200 | wenzelm | add_recdef: removed names / attributes; | file | diff | annotate |
| Fri, 30 Apr 1999 18:10:35 +0200 | wenzelm | peoper defer_recdef interface; | file | diff | annotate |
| Tue, 27 Apr 1999 10:50:08 +0200 | wenzelm | proper quiet_mode; | file | diff | annotate |
| Thu, 22 Apr 1999 12:50:39 +0200 | wenzelm | add_recdef: actual simpset; | file | diff | annotate |
| Tue, 20 Apr 1999 15:20:27 +0200 | wenzelm | temporarily fake quiet_mode; | file | diff | annotate |
| Fri, 16 Apr 1999 14:49:09 +0200 | wenzelm | 'HOL/recdef' theory data; | file | diff | annotate |
| Wed, 14 Apr 1999 19:05:10 +0200 | wenzelm | Wrapper module for Konrad Slind's TFL package. | file | diff | annotate |