2013-04-09 |
wenzelm |
discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
|
file |
diff |
annotate
|
2012-11-26 |
wenzelm |
clarified status of Legacy_XML_Syntax, despite lack of Proofterm_XML;
|
file |
diff |
annotate
|
2012-11-26 |
wenzelm |
tuned command descriptions;
|
file |
diff |
annotate
|
2012-10-17 |
wenzelm |
more formal markup;
|
file |
diff |
annotate
|
2012-08-02 |
wenzelm |
more official command specifications, including source position;
|
file |
diff |
annotate
|
2012-03-17 |
wenzelm |
slightly more parallel find_theorems;
|
file |
diff |
annotate
|
2012-03-16 |
wenzelm |
outer syntax command definitions based on formal command_spec derived from theory header declarations;
|
file |
diff |
annotate
|
2012-02-27 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
2012-02-27 |
wenzelm |
removed broken/unused introiff (cf. d452117ba564);
|
file |
diff |
annotate
|
2012-02-27 |
wenzelm |
discontinued slightly odd built-in timing (cf. 53fd5cc685b4) -- the Isar toplevel does that already (e.g. via Toplevel.timing or Toplevel.profiling);
|
file |
diff |
annotate
|
2012-02-27 |
wenzelm |
prefer uniform Timing.message -- avoid assumption about sequential execution;
|
file |
diff |
annotate
|
2011-07-12 |
wenzelm |
tuned XML modules;
|
file |
diff |
annotate
|
2011-07-10 |
wenzelm |
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
|
file |
diff |
annotate
|
2011-07-10 |
wenzelm |
simplified XML_Data;
|
file |
diff |
annotate
|
2011-07-01 |
wenzelm |
tuned layout;
|
file |
diff |
annotate
|
2011-05-30 |
krauss |
parameterize print_theorems over actual search function
|
file |
diff |
annotate
|
2011-05-30 |
krauss |
(de)serialization for search query and result
|
file |
diff |
annotate
|
2011-05-30 |
krauss |
explicit type for search queries
|
file |
diff |
annotate
|
2011-05-30 |
krauss |
moved questionable goal modification out of filter_theorems
|
file |
diff |
annotate
|
2011-05-30 |
krauss |
exported raw query parser; removed inconsistent clone
|
file |
diff |
annotate
|
2011-05-30 |
krauss |
separate query parsing from actual search
|
file |
diff |
annotate
|
2011-05-03 |
wenzelm |
more conventional naming scheme: names_long, names_short, names_unique;
|
file |
diff |
annotate
|
2011-04-16 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
2011-04-16 |
wenzelm |
Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
|
file |
diff |
annotate
|
2011-03-20 |
wenzelm |
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
|
file |
diff |
annotate
|
2011-02-25 |
krauss |
reactivate time measurement (partly reverting c27b0b37041a);
|
file |
diff |
annotate
|
2011-02-25 |
krauss |
generalize find_theorems filters to work on raw propositions, too
|
file |
diff |
annotate
|
2011-02-25 |
noschinl |
Refactor find_theorems to provide a more general filter_facts method
|
file |
diff |
annotate
|
2011-02-23 |
noschinl |
fix non-exhaustive pattern match in find_theorems
|
file |
diff |
annotate
|
2010-09-20 |
wenzelm |
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
|
file |
diff |
annotate
|
2010-08-11 |
wenzelm |
misc tuning and simplification;
|
file |
diff |
annotate
|
2010-08-11 |
wenzelm |
simplified/unified command setup;
|
file |
diff |
annotate
|
2010-05-15 |
wenzelm |
renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
|
file |
diff |
annotate
|
2010-05-15 |
wenzelm |
refer directly to structure Keyword and Parse;
|
file |
diff |
annotate
|
2010-03-07 |
wenzelm |
modernized structure Object_Logic;
|
file |
diff |
annotate
|
2010-02-27 |
wenzelm |
modernized structure Term_Ord;
|
file |
diff |
annotate
|
2009-12-14 |
haftmann |
avoid negative indices as argument ot drop
|
file |
diff |
annotate
|
2009-11-25 |
haftmann |
normalized uncurry take/drop
|
file |
diff |
annotate
|
2009-11-24 |
haftmann |
curried take/drop
|
file |
diff |
annotate
|
2009-11-29 |
kleing |
Expand nested abbreviations before applying dummy patterns.
|
file |
diff |
annotate
|
2009-11-02 |
wenzelm |
observe usual naming conventions;
|
file |
diff |
annotate
|
2009-11-02 |
krauss |
find_theorems: respect conceal flag
|
file |
diff |
annotate
|
2009-10-29 |
wenzelm |
less hermetic ML;
|
file |
diff |
annotate
|
2009-10-28 |
wenzelm |
renamed Proof.flat_goal to Proof.simple_goal;
|
file |
diff |
annotate
|
2009-10-24 |
wenzelm |
renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
|
file |
diff |
annotate
|
2009-10-21 |
haftmann |
merged
|
file |
diff |
annotate
|
2009-10-21 |
haftmann |
dropped redundant gen_ prefix
|
file |
diff |
annotate
|
2009-10-20 |
haftmann |
replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
|
file |
diff |
annotate
|
2009-10-21 |
kleing |
find_theorems: better handling of abbreviations (by Timothy Bourke)
|
file |
diff |
annotate
|
2009-10-20 |
wenzelm |
uniform use of Integer.min/max;
|
file |
diff |
annotate
|
2009-10-02 |
wenzelm |
replaced Proof.get_goal state by Proof.flat_goal state, which provides the standard view on goals for (semi)automated tools;
|
file |
diff |
annotate
|
2009-09-30 |
wenzelm |
misc tuning and simplification;
|
file |
diff |
annotate
|
2009-09-29 |
wenzelm |
explicit indication of Unsynchronized.ref;
|
file |
diff |
annotate
|
2009-07-23 |
wenzelm |
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
|
file |
diff |
annotate
|
2009-07-20 |
wenzelm |
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
|
file |
diff |
annotate
|
2009-06-17 |
wenzelm |
more detailed start_timing/end_timing;
|
file |
diff |
annotate
|
2009-06-17 |
wenzelm |
minor tuning according to Isabelle/ML conventions;
|
file |
diff |
annotate
|
2009-05-06 |
Timothy Bourke |
Prototype introiff option for find_theorems.
|
file |
diff |
annotate
|
2009-03-31 |
wenzelm |
superficial tuning;
|
file |
diff |
annotate
|
2009-03-30 |
Timothy Bourke |
Limit the number of results returned by auto_solves.
|
file |
diff |
annotate
|