src/Pure/Isar/skip_proof.ML
2009-03-05 wenzelm 2009-03-05 Thm.add_oracle interface: replaced old bstring by binding;
2009-01-21 wenzelm 2009-01-21 removed Ids;
2009-01-11 wenzelm 2009-01-11 added Goal.future_enabled abstraction -- now also checks that this is already a future task, which excludes interactive commands of the old toplevel;
2009-01-10 wenzelm 2009-01-10 added parallel_proofs flag (default true, cf. usedir option -Q), which can be disabled in low-memory situations;
2008-12-12 wenzelm 2008-12-12 future proofs: more robust check via Future.enabled;
2008-10-09 wenzelm 2008-10-09 moved future_scheduler flag to Concurrent/ROOT.ML;
2008-10-01 wenzelm 2008-10-01 renamed promise to future, tuned related interfaces;
2008-09-25 wenzelm 2008-09-25 added future_scheduler (from thy_info.ML); prove: Goal.prove_promise if future_schedule;
2008-09-18 wenzelm 2008-09-18 simplified oracle interface;
2008-04-17 wenzelm 2008-04-17 prove_global: pass context;
2008-04-03 berghofe 2008-04-03 Added prove_global.
2008-03-28 wenzelm 2008-03-28 Context.>> : operate on Context.generic;
2008-03-27 wenzelm 2008-03-27 eliminated delayed theory setup
2007-08-31 wenzelm 2007-08-31 prove: setmp quick_and_dirty (avoids race condition);
2006-08-02 wenzelm 2006-08-02 normalized Proof.context/method type aliases;
2006-07-29 wenzelm 2006-07-29 Goal.prove: more tactic arguments;
2006-07-08 wenzelm 2006-07-08 Goal.prove: context;
2006-01-19 wenzelm 2006-01-19 setup: theory -> theory;
2005-10-21 wenzelm 2005-10-21 Goal.prove;
2005-09-17 wenzelm 2005-09-17 moved quick_and_dirty to Pure/ROOT.ML;
2005-09-13 wenzelm 2005-09-13 load before proof.ML; moved proof elements to proof.ML;
2005-08-18 wenzelm 2005-08-18 accomodate interface Proof vs. Method;
2005-07-14 wenzelm 2005-07-14 tuned;
2005-04-23 wenzelm 2005-04-23 qualified name Pure.skip_proof;
2005-04-21 wenzelm 2005-04-21 superceded by Pure.thy and CPure.thy;
2005-04-07 wenzelm 2005-04-07 Thm.invoke_oracle_i;
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2001-11-28 wenzelm 2001-11-28 skip_proof: do not require quick_and_dirty in interactive mode;
2001-11-19 wenzelm 2001-11-19 improved treatment of common result name;
2001-11-11 wenzelm 2001-11-11 adapted to multiple results;
2001-11-05 wenzelm 2001-11-05 pretty/print functions with context;
2001-10-27 wenzelm 2001-10-27 added prove;
2001-10-22 wenzelm 2001-10-22 moved prove_goalw_cterm to goals.ML; cleaned up;
2001-10-12 wenzelm 2001-10-12 added make_thm (sort-of);
2000-05-05 wenzelm 2000-05-05 GPLed;
2000-03-20 wenzelm 2000-03-20 added prove_goalw_cterm; quick_and_dirty moved here;
1999-07-12 wenzelm 1999-07-12 local qed; print rule;
1999-07-08 wenzelm 1999-07-08 propp: 'concl' patterns;
1999-07-02 wenzelm 1999-07-02 skip_proof feature 'sorry' (for quick_and_dirty mode only);