src/Pure/Isar/skip_proof.ML
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