extended bib

updated generated code

added reference

subsection on locale interpretation

explicitly name and note equations for class eq

use various predefined Haskell operations when generating code

NEWS

tuned internal order

dropped unused bindings

corrected syntax diagram

turn off new polymorphism code again -- a new issue popped up

missing case

A function called "untyped_aconv" shouldn't look at the bound names!

no point in introducing combinators for inlined Skolem functions

better error reporting for Vampire

expect SPASS 3.7, and give a friendly warning if an older version is used

improve ATP-specific error messages

merged

removed simplifier congruence rule of "prod_case"

adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"

merged

declare lexn.simps [code del]

declare lex_prod_def [code del]

modernized specifications

avoid references to old constdefs

merged

disable new polymorphic code for now, until remaining issues in "equality_inf" are resolved

"raise Fail" for internal errors + one new internal error (instead of "Match")

make test work again (broken since 09467cdfa198?)

adjust Nitpick example to follow latest wave of renamings

proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter

beta-eta-contract, to respect "first_order_match"'s specification; Sledgehammer's Skolem cache sometimes failed without the contraction

adjust Nitpick's handling of "<" on "rat"s and "reals"

remove needless variables

hide sum explicitly

merged

adjust popular symbolic type constructors

tailored set of code equations manually

tuned quotes, antiquotations and whitespace

moved inductive_codegen to place where product type is available; tuned structure name

qualified type "*"; qualified constants Pair, fst, snd, split

tuned quotes, antiquotations and whitespace

qualified types "+" and nat; qualified constants Ball, Bex, Suc, curry; modernized some specifications

Adapted Mirabelle script (cf. f60e4dd6d76f)

merged

more consistent naming aroud type classes and instances

back to non-release mode;

removed obsolete test tags;

Added tag Isabelle2009-2 for changeset 35815ce9218a

final tuning;

corrected syntax diagram

Adapted Mirabelle script (cf. f60e4dd6d76f)

Added tag isa2009-2-test3 for changeset 0eacedd5f780

merged

NEWS: IsabelleText font;

Pretty.string_of (in Scala): actually observe margin/metric;

tuned Command.toString -- preserving uniqueness allows the Scala toplevel to print Linear_Set[Command] results without crashing;

tuned tooltips;

obsolete;

explicit treatment of empty exception block, which could lead to confusing output (e.g. in the theory loader), or even prevent error output altogether;

contrib/README;

removed outdated/confusing INSTALL file;

clarified font_family vs. font_family_default; install_fonts: refrain from any magic that does not really work on Mac OS, but introduces strange problems on other platforms;

disable set_styles for now -- there are still some race conditions of PropertiesChanged vs. TextArea painting (NB: without it Isabelle_Token_Marker will crash if sub/superscript is actually used);

Added tag isa2009-2-test2 for changeset dfca6c4cd1e8

more uniform treatment of options and attributes, preferring formal markup over old-style LaTeX macros;

merged;

Tuned.

Documented changes in induct, cases, and nominal_induct method.

merged

made SML/NJ happy again;

recovered some untested theories;

proper target directory;

refer to isabelle-release branch;

no symlinks; tuned;

merged

tuned ANNOUNCEMENT;

more NEWS;

more NEWS; tuned;

merged

cosmetics

renaming

show more respect for user-specified facts, even if they could lead to unsound proofs + don't throw away "unsound" theorems in "full_type" mode, since they are then sound

fix remote Vampire diagnosis

make Sledgehammer's "add:" and "del:" syntax work better in the presence of aliases; some of these aliases pop up only after Sledgehammer has converted the formula to CNF, so it can be very confusing to the user who said "add: foo del: bar" that "bar" is used in the end.

totally bypass Sledgehammer's relevance filter when facts are given using the "(fact1 ... factn)" syntax; faster and more reliable

single heaps archive;

merged

tuned;

removed obsolete dry-run option; just one archive for heaps, with the full cumulative collection (proper dependencies for rebuild);

Added tag isa2009-2-test1 for changeset d1cdbc7524b6

merged

avoid "$"

tuned whitespace

avoid flowerish abbreviation

merged

merge

don't raise Option.Option if assumptions contain schematic variables

recongize one more outcome string for "remote_vampire"

"print_vars_terms" wasn't doing its job properly; the offending line was "find_vars t1 #> find_vars t1", where the second "t1" should clearly have been "t2"

merged

made "clausify" attribute a legacy feature; seems to have ever only been a debugging feature

made "neg_clausify" a legacy feature

kill active Sledgehammer threads when running minimize, to avoid confusing the user with too much output

redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs

fix bugs in Sledgehammer's Isar proof "redirection" code

handle Vampire's definitions smoothly

fix bug in direct Isar proofs, which was exhibited by the "BigO" example

honor "xsymbols"

kill another neg_clausify proof

show types in Isar proofs, but not for free variables; this makes proofs more robust, without as much clutter as there used to be when types were enabled previously

give more helpful error message

first proposal for a announcement

NEWS (more strict internal axioms/defs format)

one all-inclusive bundle for each platform;

more robust handling of additional type variables: warning, more canonical order, drop mixfix syntax if implicit type arguments are introduced (to avoid delusion due to shifted arguments);

tuned warning;

less ambitious settings;

spelling;

do not open Proofterm, which is very ould style;