src/Pure/Isar/obtain.ML
Thu, 29 Nov 2001 01:51:06 +0100 wenzelm RuleContext.intro_query_local;
Sun, 11 Nov 2001 21:35:21 +0100 wenzelm Proof.have_i: multiple statements;
Mon, 05 Nov 2001 20:59:35 +0100 wenzelm pretty/print functions with context;
Mon, 22 Oct 2001 18:02:50 +0200 wenzelm improved source arrangement of obtain;
Tue, 16 Oct 2001 23:02:14 +0200 wenzelm simplified exporter interface;
Sun, 14 Oct 2001 20:09:19 +0200 wenzelm use ObjectLogic;
Thu, 01 Feb 2001 20:45:11 +0100 wenzelm comment
Mon, 04 Dec 2000 23:18:07 +0100 wenzelm fixed binding of parameters;
Mon, 13 Nov 2000 22:01:07 +0100 wenzelm tuned statement args;
Fri, 03 Nov 2000 21:27:06 +0100 wenzelm improved handling of "that": insert into goal, only declare as Pure "intro";
Mon, 31 Jul 2000 14:37:18 +0200 wenzelm tuned;
Sun, 30 Jul 2000 12:54:07 +0200 wenzelm turned into plain context element;
Thu, 13 Jul 2000 11:39:22 +0200 wenzelm bind_skolem;
Fri, 05 May 2000 22:09:41 +0200 wenzelm GPLed;
Thu, 30 Mar 2000 14:24:46 +0200 wenzelm ProofContext.find_free;
Tue, 21 Mar 2000 00:18:54 +0100 wenzelm handle general case: params and hyps of thesis;
Thu, 06 Jan 2000 16:00:18 +0100 wenzelm obtain: renamed 'in' to 'where';
Wed, 05 Jan 2000 11:45:01 +0100 wenzelm ObtainFun;
Fri, 22 Oct 1999 21:48:50 +0200 wenzelm warn_extra_tfrees;
Fri, 01 Oct 1999 20:38:16 +0200 wenzelm tuned comment;
Fri, 01 Oct 1999 20:36:53 +0200 wenzelm The 'obtain' language element -- achieves (eliminated) existential
less more (0) tip