Mercurial
isabelle
/ file revisions
summary
|
shortlog
|
changelog
|
graph
|
tags
|
branches
|
file
| revisions |
annotate
|
diff
|
rss
src/Pure/Isar/skip_proof.ML
2010-05-03
wenzelm
2010-05-03
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
file
|
diff
|
annotate
2010-02-07
wenzelm
2010-02-07
renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
file
|
diff
|
annotate
2009-10-17
wenzelm
2009-10-17
operations of structure Skip_Proof (formerly SkipProof) no longer require quick_and_dirty mode;
file
|
diff
|
annotate
2009-10-17
wenzelm
2009-10-17
indicate CRITICAL nature of various setmp combinators;
file
|
diff
|
annotate
2009-03-05
wenzelm
2009-03-05
Thm.add_oracle interface: replaced old bstring by binding;
file
|
diff
|
annotate
2009-01-21
wenzelm
2009-01-21
removed Ids;
file
|
diff
|
annotate
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;
file
|
diff
|
annotate
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;
file
|
diff
|
annotate
2008-12-12
wenzelm
2008-12-12
future proofs: more robust check via Future.enabled;
file
|
diff
|
annotate
2008-10-09
wenzelm
2008-10-09
moved future_scheduler flag to Concurrent/ROOT.ML;
file
|
diff
|
annotate
2008-10-01
wenzelm
2008-10-01
renamed promise to future, tuned related interfaces;
file
|
diff
|
annotate
2008-09-25
wenzelm
2008-09-25
added future_scheduler (from thy_info.ML); prove: Goal.prove_promise if future_schedule;
file
|
diff
|
annotate
2008-09-18
wenzelm
2008-09-18
simplified oracle interface;
file
|
diff
|
annotate
2008-04-17
wenzelm
2008-04-17
prove_global: pass context;
file
|
diff
|
annotate
2008-04-03
berghofe
2008-04-03
Added prove_global.
file
|
diff
|
annotate
2008-03-28
wenzelm
2008-03-28
Context.>> : operate on Context.generic;
file
|
diff
|
annotate
2008-03-27
wenzelm
2008-03-27
eliminated delayed theory setup
file
|
diff
|
annotate
2007-08-31
wenzelm
2007-08-31
prove: setmp quick_and_dirty (avoids race condition);
file
|
diff
|
annotate
2006-08-02
wenzelm
2006-08-02
normalized Proof.context/method type aliases;
file
|
diff
|
annotate
2006-07-29
wenzelm
2006-07-29
Goal.prove: more tactic arguments;
file
|
diff
|
annotate
2006-07-08
wenzelm
2006-07-08
Goal.prove: context;
file
|
diff
|
annotate
2006-01-19
wenzelm
2006-01-19
setup: theory -> theory;
file
|
diff
|
annotate
2005-10-21
wenzelm
2005-10-21
Goal.prove;
file
|
diff
|
annotate
2005-09-17
wenzelm
2005-09-17
moved quick_and_dirty to Pure/ROOT.ML;
file
|
diff
|
annotate
2005-09-13
wenzelm
2005-09-13
load before proof.ML; moved proof elements to proof.ML;
file
|
diff
|
annotate
2005-08-18
wenzelm
2005-08-18
accomodate interface Proof vs. Method;
file
|
diff
|
annotate
2005-07-14
wenzelm
2005-07-14
tuned;
file
|
diff
|
annotate
2005-04-23
wenzelm
2005-04-23
qualified name Pure.skip_proof;
file
|
diff
|
annotate
2005-04-21
wenzelm
2005-04-21
superceded by Pure.thy and CPure.thy;
file
|
diff
|
annotate
2005-04-07
wenzelm
2005-04-07
Thm.invoke_oracle_i;
file
|
diff
|
annotate
2005-02-13
skalberg
2005-02-13
Deleted Library.option type.
file
|
diff
|
annotate
2004-06-21
kleing
2004-06-21
Merged in license change from Isabelle2004
file
|
diff
|
annotate
2001-11-28
wenzelm
2001-11-28
skip_proof: do not require quick_and_dirty in interactive mode;
file
|
diff
|
annotate
2001-11-19
wenzelm
2001-11-19
improved treatment of common result name;
file
|
diff
|
annotate
2001-11-11
wenzelm
2001-11-11
adapted to multiple results;
file
|
diff
|
annotate
2001-11-05
wenzelm
2001-11-05
pretty/print functions with context;
file
|
diff
|
annotate
2001-10-27
wenzelm
2001-10-27
added prove;
file
|
diff
|
annotate
2001-10-22
wenzelm
2001-10-22
moved prove_goalw_cterm to goals.ML; cleaned up;
file
|
diff
|
annotate
2001-10-12
wenzelm
2001-10-12
added make_thm (sort-of);
file
|
diff
|
annotate
2000-05-05
wenzelm
2000-05-05
GPLed;
file
|
diff
|
annotate
2000-03-20
wenzelm
2000-03-20
added prove_goalw_cterm; quick_and_dirty moved here;
file
|
diff
|
annotate
1999-07-12
wenzelm
1999-07-12
local qed; print rule;
file
|
diff
|
annotate
1999-07-08
wenzelm
1999-07-08
propp: 'concl' patterns;
file
|
diff
|
annotate
1999-07-02
wenzelm
1999-07-02
skip_proof feature 'sorry' (for quick_and_dirty mode only);
file
|
diff
|
annotate