| Tue, 25 Jul 2006 21:18:08 +0200 | wenzelm | added find_free (from term.ML); | file | diff | annotate |
| Tue, 11 Jul 2006 12:17:11 +0200 | wenzelm | replaced Term.variant(list) by Name.variant(_list); | file | diff | annotate |
| Tue, 04 Jul 2006 19:49:55 +0200 | wenzelm | guess: proper context for polymorphic parameters; | file | diff | annotate |
| Mon, 03 Jul 2006 19:33:09 +0200 | wenzelm | obtain_export: Thm.generalize; | file | diff | annotate |
| Sat, 17 Jun 2006 19:37:47 +0200 | wenzelm | Term.internal; | file | diff | annotate |
| Thu, 15 Jun 2006 23:08:54 +0200 | wenzelm | ProofContext: moved variable operations to struct Variable; | file | diff | annotate |
| Sun, 11 Jun 2006 21:59:24 +0200 | wenzelm | fixes: include mixfix syntax; | file | diff | annotate |
| Mon, 05 Jun 2006 21:54:25 +0200 | wenzelm | guess: more careful about local polymorphism; | file | diff | annotate |
| Sun, 07 May 2006 00:22:05 +0200 | wenzelm | removed 'concl is' patterns; | file | diff | annotate |
| Thu, 27 Apr 2006 15:06:35 +0200 | wenzelm | tuned basic list operators (flat, maps, map_filter); | file | diff | annotate |
| Tue, 21 Mar 2006 12:18:07 +0100 | wenzelm | subtract (op =); | file | diff | annotate |
| Thu, 02 Feb 2006 16:31:35 +0100 | wenzelm | Proof.refine_insert; | file | diff | annotate |
| Thu, 02 Feb 2006 12:52:24 +0100 | wenzelm | obtain(_i): optional name for 'that'; | file | diff | annotate |
| Tue, 31 Jan 2006 18:19:25 +0100 | wenzelm | tuned comments; | file | diff | annotate |
| Tue, 24 Jan 2006 00:43:32 +0100 | wenzelm | ProofContext.inferred_param; | file | diff | annotate |
| Sat, 21 Jan 2006 23:02:14 +0100 | wenzelm | simplified type attribute; | file | diff | annotate |
| Sun, 15 Jan 2006 19:58:56 +0100 | wenzelm | guess: used fixed inferred_type of vars; | file | diff | annotate |
| Sat, 14 Jan 2006 17:14:06 +0100 | wenzelm | sane ERROR handling; | file | diff | annotate |
| Fri, 13 Jan 2006 01:13:11 +0100 | wenzelm | uniform handling of fixes; | file | diff | annotate |
| Tue, 10 Jan 2006 19:34:04 +0100 | wenzelm | generic attributes; | file | diff | annotate |
| Wed, 16 Nov 2005 17:45:31 +0100 | wenzelm | Term.betapplys; | file | diff | annotate |
| Thu, 10 Nov 2005 20:57:21 +0100 | wenzelm | guess: Seq.hd; | file | diff | annotate |
| Tue, 08 Nov 2005 10:44:40 +0100 | wenzelm | simplified after_qed; | file | diff | annotate |
| Fri, 28 Oct 2005 22:28:12 +0200 | wenzelm | renamed Goal constant to prop, more general protect/unprotect interfaces; | file | diff | annotate |
| Fri, 21 Oct 2005 18:14:54 +0200 | wenzelm | improved check_result; | file | diff | annotate |
| Tue, 18 Oct 2005 17:59:24 +0200 | wenzelm | tuned error msg; | file | diff | annotate |
| Sat, 15 Oct 2005 00:08:07 +0200 | wenzelm | added 'guess', which derives the obtained context from the course of reasoning; | file | diff | annotate |
| Tue, 13 Sep 2005 22:19:42 +0200 | wenzelm | tuned Isar proof elements; | file | diff | annotate |
| Thu, 18 Aug 2005 11:17:46 +0200 | wenzelm | prepare attributes here; | file | diff | annotate |
| Mon, 08 Aug 2005 22:14:04 +0200 | ballarin | After_qed takes result argument. | file | diff | annotate |
| Thu, 14 Jul 2005 19:28:24 +0200 | wenzelm | tuned; | file | diff | annotate |
| Wed, 13 Jul 2005 11:16:34 +0200 | haftmann | (intermediate commit) | file | diff | annotate |
| Wed, 29 Jun 2005 15:13:36 +0200 | wenzelm | no Syntax.internal on thesis; | 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, 27 Feb 2002 21:53:33 +0100 | wenzelm | improved messages; | file | diff | annotate |
| Thu, 06 Dec 2001 00:43:03 +0100 | wenzelm | Syntax.internal thesis; | file | diff | annotate |
| Mon, 03 Dec 2001 21:31:55 +0100 | wenzelm | renamed rule_context.ML to context_rules.ML; | file | diff | annotate |
| Thu, 29 Nov 2001 01:51:06 +0100 | wenzelm | RuleContext.intro_query_local; | file | diff | annotate |
| Sun, 11 Nov 2001 21:35:21 +0100 | wenzelm | Proof.have_i: multiple statements; | file | diff | annotate |
| Mon, 05 Nov 2001 20:59:35 +0100 | wenzelm | pretty/print functions with context; | file | diff | annotate |
| Mon, 22 Oct 2001 18:02:50 +0200 | wenzelm | improved source arrangement of obtain; | file | diff | annotate |
| Tue, 16 Oct 2001 23:02:14 +0200 | wenzelm | simplified exporter interface; | file | diff | annotate |
| Sun, 14 Oct 2001 20:09:19 +0200 | wenzelm | use ObjectLogic; | file | diff | annotate |
| Thu, 01 Feb 2001 20:45:11 +0100 | wenzelm | comment | file | diff | annotate |
| Mon, 04 Dec 2000 23:18:07 +0100 | wenzelm | fixed binding of parameters; | file | diff | annotate |
| Mon, 13 Nov 2000 22:01:07 +0100 | wenzelm | tuned statement args; | file | diff | annotate |
| Fri, 03 Nov 2000 21:27:06 +0100 | wenzelm | improved handling of "that": insert into goal, only declare as Pure "intro"; | file | diff | annotate |
| Mon, 31 Jul 2000 14:37:18 +0200 | wenzelm | tuned; | file | diff | annotate |
| Sun, 30 Jul 2000 12:54:07 +0200 | wenzelm | turned into plain context element; | file | diff | annotate |
| Thu, 13 Jul 2000 11:39:22 +0200 | wenzelm | bind_skolem; | file | diff | annotate |
| Fri, 05 May 2000 22:09:41 +0200 | wenzelm | GPLed; | file | diff | annotate |
| Thu, 30 Mar 2000 14:24:46 +0200 | wenzelm | ProofContext.find_free; | file | diff | annotate |
| Tue, 21 Mar 2000 00:18:54 +0100 | wenzelm | handle general case: params and hyps of thesis; | file | diff | annotate |
| Thu, 06 Jan 2000 16:00:18 +0100 | wenzelm | obtain: renamed 'in' to 'where'; | file | diff | annotate |
| Wed, 05 Jan 2000 11:45:01 +0100 | wenzelm | ObtainFun; | file | diff | annotate |
| Fri, 22 Oct 1999 21:48:50 +0200 | wenzelm | warn_extra_tfrees; | file | diff | annotate |
| Fri, 01 Oct 1999 20:38:16 +0200 | wenzelm | tuned comment; | file | diff | annotate |
| Fri, 01 Oct 1999 20:36:53 +0200 | wenzelm | The 'obtain' language element -- achieves (eliminated) existential | file | diff | annotate |