| 2015-06-12 |
haftmann |
uniform _ div _ as infix syntax for ring division
|
file |
diff |
annotate
|
| 2015-06-10 |
wenzelm |
merged
|
file |
diff |
annotate
|
| 2015-06-10 |
wenzelm |
support for "if prems" in local goal statements;
|
file |
diff |
annotate
|
| 2015-06-09 |
wenzelm |
more uniform treatment of auto bindings vs. explicit user bindings;
|
file |
diff |
annotate
|
| 2015-06-09 |
wenzelm |
allow for_fixes for 'have', 'show' etc.;
|
file |
diff |
annotate
|
| 2015-06-09 |
wenzelm |
clarified abstracted term bindings (again, see c8384ff11711);
|
file |
diff |
annotate
|
| 2015-06-10 |
fleury |
tuned
|
file |
diff |
annotate
|
| 2015-06-10 |
Mathias Fleury |
tuned
|
file |
diff |
annotate
|
| 2015-06-10 |
Mathias Fleury |
Renaming multiset operators < ~> <#,...
|
file |
diff |
annotate
|
| 2015-06-08 |
wenzelm |
clarified abstracted term bindings;
|
file |
diff |
annotate
|
| 2015-06-08 |
wenzelm |
more careful treatment of term bindings in 'obtain' proof body;
|
file |
diff |
annotate
|
| 2015-06-05 |
wenzelm |
added Isar command 'supply';
|
file |
diff |
annotate
|
| 2015-06-05 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2015-06-01 |
haftmann |
separate class for division operator, with particular syntax added in more specific classes
|
file |
diff |
annotate
|
| 2015-06-01 |
haftmann |
explicit argument expansion of uncheck rules;
|
file |
diff |
annotate
|
| 2015-06-01 |
wenzelm |
discontinued legacy;
|
file |
diff |
annotate
|
| 2015-05-29 |
blanchet |
removed model checks from Nitpick
|
file |
diff |
annotate
|
| 2015-05-28 |
blanchet |
made Auto Sledgehammer behave more like the real thing
|
file |
diff |
annotate
|
| 2015-05-25 |
wenzelm |
merged, resolving conflicts in Admin/isatest/settings/afp-poly and src/HOL/Tools/Nitpick/nitpick_model.ML;
|
file |
diff |
annotate
|
| 2015-05-23 |
wenzelm |
clarified NEWS: document_files are officially required since Isabelle2014, but the absence was tolerated as legacy feature;
Isabelle2015
|
file |
diff |
annotate
|
| 2015-05-17 |
wenzelm |
added Eisbach manual, using version 8845c4cb28b6 of its Bitbucket repository;
|
file |
diff |
annotate
|
| 2015-05-07 |
wenzelm |
use display_graph_old for locale_deps, to show a bit more than nothing for cyclic graphs;
|
file |
diff |
annotate
|
| 2015-05-05 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2015-05-04 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2015-05-04 |
kuncar |
NEWS
|
file |
diff |
annotate
|
| 2015-05-04 |
nipkow |
no more simp_legacy_precond
|
file |
diff |
annotate
|
| 2015-04-19 |
wenzelm |
back to post-release mode -- after fork point;
|
file |
diff |
annotate
|
| 2015-04-17 |
wenzelm |
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
|
file |
diff |
annotate
|
| 2015-04-17 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2015-04-17 |
wenzelm |
tuned for release;
|
file |
diff |
annotate
|
| 2015-04-17 |
traytel |
(low importance) NEWS
|
file |
diff |
annotate
|
| 2015-04-17 |
wenzelm |
allow to exclude session groups;
|
file |
diff |
annotate
|
| 2015-04-16 |
wenzelm |
explicit error for Toplevel.proof_of;
|
file |
diff |
annotate
|
| 2015-04-16 |
wenzelm |
clarified thy_deps;
|
file |
diff |
annotate
|
| 2015-04-16 |
wenzelm |
let the system choose Graph_Display.display_graph_old: thm_deps needs tree hierarchy, code_deps needs cycles (!?);
|
file |
diff |
annotate
|
| 2015-04-15 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| 2015-04-14 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| 2015-04-11 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2015-04-11 |
paulson |
Complex roots of unity. Better definition of ln for complex numbers. Used [code del] to stop code generation for powr.
|
file |
diff |
annotate
|
| 2015-04-11 |
wenzelm |
tuned spelling;
|
file |
diff |
annotate
|
| 2015-04-11 |
wenzelm |
misc tuning for release;
|
file |
diff |
annotate
|
| 2015-04-10 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2015-04-10 |
nipkow |
renamed Multiset.fold -> fold_mset, Multiset.filter -> filter_mset
|
file |
diff |
annotate
|
| 2015-04-09 |
wenzelm |
merged
|
file |
diff |
annotate
|
| 2015-04-09 |
wenzelm |
clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);
|
file |
diff |
annotate
|
| 2015-04-09 |
blanchet |
introduced new abbreviations for multiset operations (in the hope of getting rid of the old names <, <=, etc.)
|
file |
diff |
annotate
|
| 2015-04-08 |
blanchet |
tuned wording
|
file |
diff |
annotate
|
| 2015-04-08 |
blanchet |
Z3 news
|
file |
diff |
annotate
|
| 2015-04-08 |
blanchet |
renamed multiset ordering to free up nice <# etc. symbols for the standard subset
|
file |
diff |
annotate
|
| 2015-04-08 |
wenzelm |
misc tuning for release;
|
file |
diff |
annotate
|
| 2015-04-07 |
nipkow |
Removed mcard because it is equal to size
|
file |
diff |
annotate
|
| 2015-04-06 |
wenzelm |
support for 'restricted' modifier: only qualified accesses outside the local scope;
|
file |
diff |
annotate
|
| 2015-04-06 |
wenzelm |
@{command_spec} is superseded by @{command_keyword};
|
file |
diff |
annotate
|
| 2015-04-04 |
wenzelm |
some explanation of 'private';
|
file |
diff |
annotate
|
| 2015-04-01 |
wenzelm |
merged
|
file |
diff |
annotate
|
| 2015-04-01 |
wenzelm |
added command 'experiment';
|
file |
diff |
annotate
|
| 2015-04-01 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| 2015-04-01 |
wenzelm |
added isabelle build option -x, to exclude sessions;
|
file |
diff |
annotate
|
| 2015-04-01 |
wenzelm |
added isabelle build option -k, for fast off-line checking of theory sources;
|
file |
diff |
annotate
|
| 2015-04-01 |
paulson |
HOL Light Libraries for complex Arctan, Arcsin, Arccos
|
file |
diff |
annotate
|