src/Pure/Isar/skip_proof.ML
2011-04-19 ago added more elementary Skip_Proof.make_thm_cterm;
2011-04-16 ago modernized structure Proof_Context;
2010-05-03 ago renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-02-07 ago renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
2009-10-17 ago operations of structure Skip_Proof (formerly SkipProof) no longer require quick_and_dirty mode;
2009-10-17 ago indicate CRITICAL nature of various setmp combinators;
2009-03-05 ago Thm.add_oracle interface: replaced old bstring by binding;
2009-01-21 ago removed Ids;
2009-01-11 ago added Goal.future_enabled abstraction -- now also checks that this is already
2009-01-10 ago added parallel_proofs flag (default true, cf. usedir option -Q), which can be disabled in low-memory situations;
2008-12-12 ago future proofs: more robust check via Future.enabled;
2008-10-09 ago moved future_scheduler flag to Concurrent/ROOT.ML;
2008-10-01 ago renamed promise to future, tuned related interfaces;
2008-09-25 ago added future_scheduler (from thy_info.ML);
2008-09-18 ago simplified oracle interface;
2008-04-17 ago prove_global: pass context;
2008-04-03 ago Added prove_global.
2008-03-28 ago Context.>> : operate on Context.generic;
2008-03-27 ago eliminated delayed theory setup
2007-08-31 ago prove: setmp quick_and_dirty (avoids race condition);
2006-08-02 ago normalized Proof.context/method type aliases;
2006-07-29 ago Goal.prove: more tactic arguments;
2006-07-08 ago Goal.prove: context;
2006-01-19 ago setup: theory -> theory;
2005-10-21 ago Goal.prove;
2005-09-17 ago moved quick_and_dirty to Pure/ROOT.ML;
2005-09-13 ago load before proof.ML;
2005-08-18 ago accomodate interface Proof vs. Method;
2005-07-14 ago tuned;
2005-04-23 ago qualified name Pure.skip_proof;
2005-04-21 ago superceded by Pure.thy and CPure.thy;
2005-04-07 ago Thm.invoke_oracle_i;
2005-02-13 ago Deleted Library.option type.
2004-06-21 ago Merged in license change from Isabelle2004
2001-11-28 ago skip_proof: do not require quick_and_dirty in interactive mode;
2001-11-19 ago improved treatment of common result name;
2001-11-11 ago adapted to multiple results;
2001-11-05 ago pretty/print functions with context;
2001-10-27 ago added prove;
2001-10-22 ago moved prove_goalw_cterm to goals.ML;
2001-10-12 ago added make_thm (sort-of);
2000-05-05 ago GPLed;
2000-03-20 ago added prove_goalw_cterm;
1999-07-12 ago local qed; print rule;
1999-07-08 ago propp: 'concl' patterns;
1999-07-02 ago skip_proof feature 'sorry' (for quick_and_dirty mode only);