| 2014-02-12 |
blanchet |
[mq]: news
|
file |
diff |
annotate
|
| 2014-02-10 |
wenzelm |
discontinued axiomatic 'classes', 'classrel', 'arities';
|
file |
diff |
annotate
|
| 2014-02-04 |
Lars Hupel |
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
|
file |
diff |
annotate
|
| 2014-02-04 |
blanchet |
removed legacy 'metisFT' method
|
file |
diff |
annotate
|
| 2014-02-03 |
blanchet |
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
|
file |
diff |
annotate
|
| 2014-02-03 |
blanchet |
added new option to documentation
|
file |
diff |
annotate
|
| 2014-01-30 |
blanchet |
renamed Sledgehammer options for symmetry between positive and negative versions
|
file |
diff |
annotate
|
| 2014-01-26 |
wenzelm |
discontinued obsolete attribute "standard";
|
file |
diff |
annotate
|
| 2014-01-25 |
wenzelm |
explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
|
file |
diff |
annotate
|
| 2014-01-25 |
wenzelm |
NEWS for 31afce809794;
|
file |
diff |
annotate
|
| 2014-01-22 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| 2014-01-22 |
wenzelm |
merged
|
file |
diff |
annotate
|
| 2014-01-22 |
wenzelm |
inner syntax token language allows regular quoted strings;
|
file |
diff |
annotate
|
| 2014-01-21 |
blanchet |
updated NEWS
|
file |
diff |
annotate
|
| 2014-01-19 |
boehmes |
removed obsolete remote_cvc3 and remote_z3
|
file |
diff |
annotate
|
| 2014-01-17 |
wenzelm |
clarified @{rail} syntax: prefer explicit \<newline> symbol;
|
file |
diff |
annotate
|
| 2014-01-15 |
wenzelm |
added \<newline> symbol, which is used for char/string literals in HOL;
|
file |
diff |
annotate
|
| 2014-01-13 |
wenzelm |
activation of Z3 via "z3_non_commercial" system option (without requiring restart);
|
file |
diff |
annotate
|
| 2014-01-13 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2014-01-12 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| 2014-01-01 |
wenzelm |
avoid unicode text, which causes problems when recoding symbols (e.g. via UTF8-Isabelle in Isabelle/jEdit);
|
file |
diff |
annotate
|
| 2014-01-01 |
haftmann |
fundamental treatment of undefined vs. universally partial replaces code_abort
|
file |
diff |
annotate
|
| 2013-12-30 |
wenzelm |
added system option "jedit_print_mode";
|
file |
diff |
annotate
|
| 2013-12-25 |
haftmann |
abolished slightly odd global lattice interpretation for min/max
|
file |
diff |
annotate
|
| 2013-12-23 |
haftmann |
NEWS
|
file |
diff |
annotate
|
| 2013-12-17 |
immler |
NEWS
|
file |
diff |
annotate
|
| 2013-12-15 |
haftmann |
disambiguation of interpretation prefixes
|
file |
diff |
annotate
|
| 2013-12-14 |
wenzelm |
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
|
file |
diff |
annotate
|
| 2013-12-12 |
wenzelm |
discontinued legacy_isub_isup;
|
file |
diff |
annotate
|
| 2013-12-09 |
haftmann |
NEWS
|
file |
diff |
annotate
|
| 2013-12-09 |
wenzelm |
provide @{file_unchecked} in Isabelle/Pure;
|
file |
diff |
annotate
|
| 2013-12-09 |
wenzelm |
added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
|
file |
diff |
annotate
|
| 2013-12-06 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| 2013-12-06 |
wenzelm |
clarified "isabelle display" and 'display_drafts': re-use file and program instance, open asynchronously via desktop environment;
|
file |
diff |
annotate
|
| 2013-12-05 |
wenzelm |
relocate NEWS to post-release version (cf. 7a14f831d02d);
|
file |
diff |
annotate
|
| 2013-12-05 |
wenzelm |
merged, resolving obvious conflicts in NEWS and src/Pure/System/isabelle_process.ML;
|
file |
diff |
annotate
|
| 2013-12-01 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2013-11-30 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| 2013-11-25 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| 2013-11-21 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| 2013-11-20 |
wenzelm |
updated to Isabelle2013-2;
|
file |
diff |
annotate
|
| 2013-12-05 |
blanchet |
make sure acyclicity axiom gets generated in the case where the problem involves mutually recursive datatypes
|
file |
diff |
annotate
|
| 2013-12-05 |
Andreas Lochbihler |
news
|
file |
diff |
annotate
|
| 2013-11-26 |
traytel |
NEWS
|
file |
diff |
annotate
|
| 2013-11-25 |
haftmann |
even more precise NEWS
|
file |
diff |
annotate
|
| 2013-11-20 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| 2013-11-19 |
haftmann |
more correct NEWS
|
file |
diff |
annotate
|
| 2013-11-19 |
haftmann |
eliminiated neg_numeral in favour of - (numeral _)
|
file |
diff |
annotate
|
| 2013-11-16 |
wenzelm |
toplevel function "use" refers to raw ML bootstrap environment;
|
file |
diff |
annotate
|
| 2013-11-11 |
wenzelm |
merged, using src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML and src/HOL/Tools/Sledgehammer/sledgehammer_run.ML from 347c3b0cab44;
|
file |
diff |
annotate
|
| 2013-11-09 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| 2013-11-05 |
wenzelm |
no default shortcut for isabelle.reset-font-size -- avoid conflict with unsplit-current;
|
file |
diff |
annotate
|
| 2013-10-30 |
wenzelm |
more on file-system access;
|
file |
diff |
annotate
|
| 2013-10-14 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2013-10-09 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| 2013-10-04 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| 2013-11-10 |
haftmann |
qualifed popular user space names
|
file |
diff |
annotate
|
| 2013-11-05 |
hoelzl |
NEWS
|
file |
diff |
annotate
|
| 2013-11-04 |
haftmann |
fact generalization and name consolidation
|
file |
diff |
annotate
|
| 2013-11-01 |
haftmann |
more simplification rules on unary and binary minus
|
file |
diff |
annotate
|