| Thu, 31 May 2007 23:47:36 +0200 | wenzelm | simplified/unified list fold; | file | diff | annotate |
| Fri, 13 Apr 2007 16:40:16 +0200 | haftmann | canonical merge operations | file | diff | annotate |
| Wed, 07 Feb 2007 18:04:44 +0100 | berghofe | Added functions hhf_proof and un_hhf_proof. | file | diff | annotate |
| Tue, 05 Dec 2006 00:30:38 +0100 | wenzelm | thm/prf: separate official name vs. additional tags; | file | diff | annotate |
| Thu, 21 Sep 2006 19:04:20 +0200 | wenzelm | member (op =); | file | diff | annotate |
| Tue, 11 Jul 2006 12:17:01 +0200 | wenzelm | Name.invent_list; | file | diff | annotate |
| Thu, 27 Apr 2006 15:06:35 +0200 | wenzelm | tuned basic list operators (flat, maps, map_filter); | file | diff | annotate |
| Wed, 26 Apr 2006 22:38:05 +0200 | wenzelm | tuned; | file | diff | annotate |
| Tue, 25 Apr 2006 22:23:41 +0200 | wenzelm | tuned; | file | diff | annotate |
| Tue, 21 Mar 2006 12:18:20 +0100 | wenzelm | avoid polymorphic equality; | file | diff | annotate |
| Wed, 22 Feb 2006 22:18:41 +0100 | wenzelm | rew: handle conjunctionI/D1/D2; | file | diff | annotate |
| Thu, 19 Jan 2006 21:22:08 +0100 | wenzelm | setup: theory -> theory; | file | diff | annotate |
| Wed, 16 Nov 2005 17:45:31 +0100 | wenzelm | Term.betapplys; | file | diff | annotate |
| Fri, 28 Oct 2005 22:27:51 +0200 | wenzelm | renamed Goal constant to prop; | file | diff | annotate |
| Fri, 21 Oct 2005 18:14:59 +0200 | wenzelm | renamed triv_goal to goalI, rev_triv_goal to goalD; | file | diff | annotate |
| Wed, 31 Aug 2005 15:46:40 +0200 | wenzelm | refer to theory instead of low-level tsig; | file | diff | annotate |
| Tue, 23 Aug 2005 09:18:44 +0200 | haftmann | replaced ? by ?? | file | diff | annotate |
| Wed, 03 Aug 2005 16:25:22 +0200 | berghofe | Adapted to new interface of thms_of_proof. | file | diff | annotate |
| Fri, 15 Jul 2005 15:44:15 +0200 | wenzelm | tuned fold on terms; | file | diff | annotate |
| Wed, 13 Jul 2005 11:16:34 +0200 | haftmann | (intermediate commit) | file | diff | annotate |
| Thu, 21 Apr 2005 22:02:06 +0200 | wenzelm | superceded by Pure.thy and CPure.thy; | file | diff | annotate |
| Fri, 04 Mar 2005 15:07:34 +0100 | skalberg | Removed practically all references to Library.foldr. | file | diff | annotate |
| Thu, 03 Mar 2005 12:43:01 +0100 | skalberg | Move towards standard functions. | file | diff | annotate |
| Sun, 13 Feb 2005 17:15:14 +0100 | skalberg | Deleted Library.option type. | file | diff | annotate |
| Mon, 21 Jun 2004 10:25:57 +0200 | kleing | Merged in license change from Isabelle2004 | file | diff | annotate |
| Wed, 23 Apr 2003 00:13:32 +0200 | berghofe | elim_vars now handles both Vars and Frees. | file | diff | annotate |
| Mon, 14 Oct 2002 10:44:32 +0200 | nipkow | Ported find_intro/elim to Isar. | file | diff | annotate |
| Mon, 30 Sep 2002 16:40:57 +0200 | berghofe | Added function elim_vars. | file | diff | annotate |
| Wed, 10 Jul 2002 18:37:51 +0200 | berghofe | - Moved abs_def to drule.ML | file | diff | annotate |
| Fri, 28 Jun 2002 19:51:40 +0200 | berghofe | Additional rule for rewriting on ==. | file | diff | annotate |
| Fri, 31 May 2002 18:50:03 +0200 | berghofe | Changed interface of Pattern.rewrite_term. | file | diff | annotate |
| Wed, 20 Feb 2002 15:56:26 +0100 | berghofe | New function for eliminating definitions in proof term. | file | diff | annotate |
| Sat, 02 Feb 2002 13:26:51 +0100 | berghofe | Rewrite procedure now works for both compact and full proof objects. | file | diff | annotate |
| Mon, 19 Nov 2001 17:40:07 +0100 | berghofe | Added setup. | file | diff | annotate |
| Wed, 31 Oct 2001 20:00:35 +0100 | berghofe | Additional rules for simplifying inside "Goal" | file | diff | annotate |
| Fri, 28 Sep 2001 11:04:44 +0200 | berghofe | Exchanged % and %%. | file | diff | annotate |
| Fri, 31 Aug 2001 18:46:48 +0200 | wenzelm | tuned headers; | file | diff | annotate |
| Fri, 31 Aug 2001 16:17:05 +0200 | berghofe | Initial revision of tools for proof terms. | file | diff | annotate |