src/Pure/Isar/skip_proof.ML
Tue, 19 Apr 2011 22:08:42 +0200 wenzelm added more elementary Skip_Proof.make_thm_cterm;
Sat, 16 Apr 2011 15:47:52 +0200 wenzelm modernized structure Proof_Context;
Mon, 03 May 2010 14:25:56 +0200 wenzelm renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
Sun, 07 Feb 2010 19:33:34 +0100 wenzelm renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
Sat, 17 Oct 2009 16:58:03 +0200 wenzelm operations of structure Skip_Proof (formerly SkipProof) no longer require quick_and_dirty mode;
Sat, 17 Oct 2009 15:57:51 +0200 wenzelm indicate CRITICAL nature of various setmp combinators;
Thu, 05 Mar 2009 19:48:02 +0100 wenzelm Thm.add_oracle interface: replaced old bstring by binding;
Wed, 21 Jan 2009 23:21:44 +0100 wenzelm removed Ids;
Sun, 11 Jan 2009 18:18:35 +0100 wenzelm added Goal.future_enabled abstraction -- now also checks that this is already
Sat, 10 Jan 2009 21:32:30 +0100 wenzelm added parallel_proofs flag (default true, cf. usedir option -Q), which can be disabled in low-memory situations;
Fri, 12 Dec 2008 12:14:02 +0100 wenzelm future proofs: more robust check via Future.enabled;
Thu, 09 Oct 2008 20:53:21 +0200 wenzelm moved future_scheduler flag to Concurrent/ROOT.ML;
Wed, 01 Oct 2008 12:18:18 +0200 wenzelm renamed promise to future, tuned related interfaces;
Thu, 25 Sep 2008 20:34:20 +0200 wenzelm added future_scheduler (from thy_info.ML);
Thu, 18 Sep 2008 19:39:44 +0200 wenzelm simplified oracle interface;
Thu, 17 Apr 2008 22:22:21 +0200 wenzelm prove_global: pass context;
Thu, 03 Apr 2008 17:43:01 +0200 berghofe Added prove_global.
Fri, 28 Mar 2008 20:02:04 +0100 wenzelm Context.>> : operate on Context.generic;
Thu, 27 Mar 2008 15:32:15 +0100 wenzelm eliminated delayed theory setup
Fri, 31 Aug 2007 18:46:37 +0200 wenzelm prove: setmp quick_and_dirty (avoids race condition);
Wed, 02 Aug 2006 22:26:41 +0200 wenzelm normalized Proof.context/method type aliases;
Sat, 29 Jul 2006 00:51:29 +0200 wenzelm Goal.prove: more tactic arguments;
Sat, 08 Jul 2006 12:54:37 +0200 wenzelm Goal.prove: context;
Thu, 19 Jan 2006 21:22:08 +0100 wenzelm setup: theory -> theory;
Fri, 21 Oct 2005 18:14:34 +0200 wenzelm Goal.prove;
Sat, 17 Sep 2005 19:17:35 +0200 wenzelm moved quick_and_dirty to Pure/ROOT.ML;
Tue, 13 Sep 2005 22:19:47 +0200 wenzelm load before proof.ML;
Thu, 18 Aug 2005 11:17:49 +0200 wenzelm accomodate interface Proof vs. Method;
Thu, 14 Jul 2005 19:28:24 +0200 wenzelm tuned;
Sat, 23 Apr 2005 19:51:04 +0200 wenzelm qualified name Pure.skip_proof;
Thu, 21 Apr 2005 22:02:06 +0200 wenzelm superceded by Pure.thy and CPure.thy;
Thu, 07 Apr 2005 09:26:55 +0200 wenzelm Thm.invoke_oracle_i;
Sun, 13 Feb 2005 17:15:14 +0100 skalberg Deleted Library.option type.
Mon, 21 Jun 2004 10:25:57 +0200 kleing Merged in license change from Isabelle2004
Wed, 28 Nov 2001 23:31:47 +0100 wenzelm skip_proof: do not require quick_and_dirty in interactive mode;
Mon, 19 Nov 2001 23:37:01 +0100 wenzelm improved treatment of common result name;
Sun, 11 Nov 2001 21:37:44 +0100 wenzelm adapted to multiple results;
Mon, 05 Nov 2001 20:59:35 +0100 wenzelm pretty/print functions with context;
Sat, 27 Oct 2001 23:19:55 +0200 wenzelm added prove;
Mon, 22 Oct 2001 18:03:49 +0200 wenzelm moved prove_goalw_cterm to goals.ML;
Fri, 12 Oct 2001 12:09:38 +0200 wenzelm added make_thm (sort-of);
Fri, 05 May 2000 22:09:41 +0200 wenzelm GPLed;
Mon, 20 Mar 2000 18:48:12 +0100 wenzelm added prove_goalw_cterm;
Mon, 12 Jul 1999 22:28:56 +0200 wenzelm local qed; print rule;
Thu, 08 Jul 1999 18:36:09 +0200 wenzelm propp: 'concl' patterns;
Fri, 02 Jul 1999 19:04:32 +0200 wenzelm skip_proof feature 'sorry' (for quick_and_dirty mode only);
less more (0) tip