| 2010-05-15 |
wenzelm |
renamed structure SpecParse to Parse_Spec, keeping the old name as alias for some time;
|
file |
diff |
annotate
|
| 2010-05-15 |
wenzelm |
renamed structure OuterKeyword to Keyword and OuterParse to Parse, keeping the old names as legacy aliases for some time;
|
file |
diff |
annotate
|
| 2010-05-14 |
blanchet |
added some Sledgehammer news
|
file |
diff |
annotate
|
| 2010-05-14 |
blanchet |
document Nitpick changes
|
file |
diff |
annotate
|
| 2010-05-13 |
nipkow |
Multiset: renamed, added and tuned lemmas;
|
file |
diff |
annotate
|
| 2010-05-12 |
wenzelm |
minor tuning;
|
file |
diff |
annotate
|
| 2010-05-12 |
wenzelm |
reverted parts of 7902dc7ea11d -- note that NEWS of published Isabelle releases are essentially read-only;
|
file |
diff |
annotate
|
| 2010-05-12 |
hoelzl |
clarified NEWS entry
|
file |
diff |
annotate
|
| 2010-05-12 |
hoelzl |
merged
|
file |
diff |
annotate
|
| 2010-05-12 |
hoelzl |
added NEWS entry
|
file |
diff |
annotate
|
| 2010-05-11 |
huffman |
removed lemma real_sq_order; use power2_le_imp_le instead
|
file |
diff |
annotate
|
| 2010-05-11 |
huffman |
fix spelling of 'superseded'
|
file |
diff |
annotate
|
| 2010-05-11 |
huffman |
NEWS: removed theory PReal
|
file |
diff |
annotate
|
| 2010-05-11 |
huffman |
collected NEWS updates for HOLCF
|
file |
diff |
annotate
|
| 2010-05-11 |
haftmann |
renamed former Int.int_induct to Int.int_of_nat_induct, former Presburger.int_induct to Int.int_induct: is more conservative and more natural than the intermediate solution
|
file |
diff |
annotate
|
| 2010-05-11 |
haftmann |
theorem Presburger.int_induct has been renamed to Int.int_bidirectional_induct
|
file |
diff |
annotate
|
| 2010-05-06 |
haftmann |
dropped duplicate comp_arith
|
file |
diff |
annotate
|
| 2010-05-04 |
wenzelm |
merged
|
file |
diff |
annotate
|
| 2010-05-04 |
haftmann |
NEWS
|
file |
diff |
annotate
|
| 2010-05-03 |
wenzelm |
old NEWS on global operations;
|
file |
diff |
annotate
|
| 2010-04-29 |
wenzelm |
removed some Emacs junk;
|
file |
diff |
annotate
|
| 2010-04-29 |
haftmann |
merged
|
file |
diff |
annotate
|
| 2010-04-29 |
haftmann |
NEWS: code_reflect
|
file |
diff |
annotate
|
| 2010-04-29 |
wenzelm |
allow concrete syntax for local entities within a proof body, either via regular mixfix annotations to 'fix' etc. or the separate 'write' command;
|
file |
diff |
annotate
|
| 2010-04-28 |
haftmann |
merged
|
file |
diff |
annotate
|
| 2010-04-28 |
haftmann |
empty class specifcations observe default sort
|
file |
diff |
annotate
|
| 2010-04-28 |
wenzelm |
command 'defaultsort' is renamed to 'default_sort', it works within a local theory context;
|
file |
diff |
annotate
|
| 2010-04-28 |
haftmann |
term_typ: print styled term
|
file |
diff |
annotate
|
| 2010-04-27 |
wenzelm |
monotonic sort certification: sorts are no longer minimized at the kernel boundary, only when reading input from the end-user;
|
file |
diff |
annotate
|
| 2010-04-27 |
haftmann |
NEWS and CONTRIBUTORS
|
file |
diff |
annotate
|
| 2010-04-26 |
wenzelm |
command 'example_proof' opens an empty proof body;
|
file |
diff |
annotate
|
| 2010-04-26 |
haftmann |
dropped group_simps, ring_simps, field_eq_simps; classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero
|
file |
diff |
annotate
|
| 2010-04-23 |
wenzelm |
explicit 'schematic_theorem' etc. for schematic theorem statements;
|
file |
diff |
annotate
|
| 2010-04-23 |
haftmann |
modernized abstract algebra theories
|
file |
diff |
annotate
|
| 2010-04-19 |
wenzelm |
polyml-platform script is superseded by ISABELLE_PLATFORM;
|
file |
diff |
annotate
|
| 2010-04-16 |
wenzelm |
keep localized 'types' as regular non-old-style version -- 'type_abbrev' as 'type' just causes too many problems, e.g. clash with "type" in translations or "type:" argument syntax;
|
file |
diff |
annotate
|
| 2010-04-16 |
wenzelm |
separate commands 'hide_class', 'hide_type', 'hide_const', 'hide_fact';
|
file |
diff |
annotate
|
| 2010-04-16 |
wenzelm |
added ML antiquotation @{make_string}, which produces proper pretty printed version in Poly/ML 5.3.0 or later;
|
file |
diff |
annotate
|
| 2010-04-15 |
haftmann |
theory RBT with abstract type of red-black trees backed by implementation RBT_Impl
|
file |
diff |
annotate
|
| 2010-04-07 |
ballarin |
Merged resolving conflicts NEWS and locale.ML.
|
file |
diff |
annotate
|
| 2010-02-15 |
ballarin |
Graceful treatment of non-locale subgoals by methods unfold_locales and intro_locales.
|
file |
diff |
annotate
|
| 2010-03-30 |
krauss |
NEWS
|
file |
diff |
annotate
|
| 2010-03-28 |
wenzelm |
configuration options admit dynamic default values;
|
file |
diff |
annotate
|
| 2010-03-27 |
boehmes |
re-introduce reference to control simplifier tracing (needed for ProofGeneral settings menu) (cf. 12bb31230550)
|
file |
diff |
annotate
|
| 2010-03-26 |
boehmes |
replaced references 'trace_simp' and 'debug_simp' by configuration options stored in the context
|
file |
diff |
annotate
|
| 2010-03-20 |
wenzelm |
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
|
file |
diff |
annotate
|
| 2010-03-17 |
huffman |
NEWS: Nat_Bijection library
|
file |
diff |
annotate
|
| 2010-03-13 |
wenzelm |
local theory specifications handle hidden polymorphism implicitly;
|
file |
diff |
annotate
|
| 2010-03-13 |
wenzelm |
removed obsolete HOL/Library/Coinductive_List.thy, superceded by thys/Coinductive/Coinductive_List.thy in AFP/f2f5727b77d0;
|
file |
diff |
annotate
|
| 2010-03-13 |
wenzelm |
command 'typedef' now works within a local theory context;
|
file |
diff |
annotate
|
| 2010-03-11 |
haftmann |
NEWS
|
file |
diff |
annotate
|
| 2010-03-11 |
haftmann |
fixed typo
|
file |
diff |
annotate
|
| 2010-03-09 |
wenzelm |
localized typedecl;
|
file |
diff |
annotate
|
| 2010-03-06 |
wenzelm |
eliminated Args.bang_facts (legacy feature);
|
file |
diff |
annotate
|
| 2010-03-03 |
wenzelm |
authentic syntax for *all* logical entities;
|
file |
diff |
annotate
|
| 2010-03-01 |
wenzelm |
added type_notation command;
|
file |
diff |
annotate
|
| 2010-02-27 |
wenzelm |
clarified @{const_name} (only logical consts) vs. @{const_abbrev};
|
file |
diff |
annotate
|
| 2010-02-27 |
wenzelm |
ML antiquotations for type classes;
|
file |
diff |
annotate
|
| 2010-02-26 |
haftmann |
merged
|
file |
diff |
annotate
|
| 2010-02-24 |
haftmann |
renamed theory Rational to Rat
|
file |
diff |
annotate
|