proper update_header;

refined node_header -- more direct buffer access (again);

merged

improved handling of polymorphic quotient types, by avoiding comparing types that will generally differ in the polymorphic case

fixed handling of "Rep_" function of quotient types -- side-effect of "set" constructor reintroduction

more robust set element extractor

fine-tune intended failure of smt method when the chosen SMT solver is not installed: restrict failures to true invocations of the SMT solver and don't fail for runs based on certificates

tuned proofs;

more tolerant cygpath invocation, allow empty CLASSPATH;

explicitly revoke delay, to avoid spurious timer events after deactivation of related components;

clarified document nodes (full import graph) vs. node_status (non-preloaded theories); tuned;

more defensive node_header;

clarified module Thy_Load; more precise graph based on Document.Node.Deps with actual Node.Name dependencies;

SMT fails if the chosen SMT solver is not installed

merged

speed up Sledgehammer's clasimpset lookup a bit

use SPASS instead of E for Metis examples -- it's seems faster for these small problems

spelling

avoid undeclared variables in let bindings; tuned proofs;

tuned proofs;

more release tests;

display proof results as "state", to suppress odd squiggles in the Prover IDE (see also 9240be8c8c69);

Finish localizing the quotient package.

merged

Added infrastructure for mapping SPARK field / constructor names to Isabelle types

Use long prefix rather than short package name to disambiguate constant names introduced by verification environment

more explicit development graph;

removed dead code (cf. a34d89ce6097);

tuned proofs;

tuned proofs;

removed introiff (cf. b09afce1e54f);

tuned;

removed broken/unused introiff (cf. d452117ba564);

discontinued slightly odd built-in timing (cf. 53fd5cc685b4) -- the Isar toplevel does that already (e.g. via Toplevel.timing or Toplevel.profiling);

tuned;

tuned proofs;

prefer uniform Timing.message -- avoid assumption about sequential execution;

prefer final ADTs -- prevent ooddities;

more explicit Long_Name operations (NB: analyzing qualifiers is inherently fragile);

more standard settings -- refer to COMPONENT at most once;

clarified prems_lin_arith_tac, with subtle change of semantics: structured prems are inserted as well;

prefer cut_tac, where it is clear that the special variants cut_rules_tac or cut_facts_tac are not required;

eliminated odd comment from distant past;

updated cut_tac, without loose references to implementation manual;

updated generated file;

simplified cut_tac (cf. d549b5b0f344);

merged

avoid using constant Int.neg

reactivated Find_Unused_Assms_Examples to avoid untested / dead stuff in the repository; moved the whole HOL-Quickcheck_Examples target from "all" to "full" for now -- it does not terminate in certain situations (to be investigated further);

merged

added lemma

converting "set [...]" to "{...}" in evaluation results

removing Find_Unused_Assms_Examples from session as it requires much time

restored accidental omission

dropped dead code

tuned structure

retain syntax here

tuned structure; dropped already existing syntax declarations

tuned syntax declarations; tuned structure

merged

marked candidates for rule declarations

include warning messages in node status;

tuned signature (in accordance with ML);

more PIDE modules;

tuned proofs;

more abstract class Document.State;

more abstract class Document.State.Assignment;

tuned signature;

more abstract class Document.Version; tuned (NB: Version.nodes is total);

more abstract class Document.Node;

more abstract class Document.History;

more abstract class Document.Change;

tuned;

tuned signature; clarified check;

merged

slightly changing the enumeration scheme

adding some more test invocations of find_unused_assms

adding an example where random beats exhaustive testing

removing unnecessary assumptions in RComplete; simplifying proof in Probability

removing unnecessary assumptions in RealDef; simplifying proofs in Float, MIR, and Ferrack

one general list_all2_update_cong instead of two special ones

tuned comments;

standard Graph instances;

clarified signature -- avoid oddities of Iterable like Iterator.map; specific toString;

discontinued slightly odd Graph.del_nodes (inefficient due to full Table.map);

moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy

explicit is better than implicit

dropped dead code

prefer sorted Map/Set for canonical order of results -- pass ordering via fresh copy of empty; discontinued map_nodes, del_nodes conveniences -- avoid inefficient mapValues wrapper (this is not Table.map from ML); tuned signature;

tuned imports;

tuned signature;

discontinued obsolete Graph.all_paths (last seen in 1524d69783d3 and AFP/80bbbdbfec62);

merged

remove ill-formed lemmas word_0_wi_Pls and word_m1_wi_Min

avoid using Int.succ_def in proofs

avoid using Int.succ or Int.pred in proofs

avoid using BIT_simps in proofs; rephrase lemmas without Int.succ or Int.pred;

avoid using BIT_simps in proofs

updated stats according to src/HOL/IsaMakefile;

more precise clean target;

clarifed name space "type name", which covers logical and non-logical types, and often occurs inside outer syntax "type" markup;

avoid using Int.Pls_def in proofs

remove ill-formed lemmas word_pred_0_Min and word_m1_Min

remove ill-formed lemma of_bl_no; adapt proofs

adapt lemma mask_lem to respect int/bin distinction

rephrase some slow "metis" calls

added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)

general solution to the arity bug that occasionally plagues Sledgehammer -- short story, lots of things go kaputt when a polymorphic symbol's arity in the translation is higher than the arity of the fully polymorphic HOL constant

renamed 'try_methods' to 'try0'

doc fixes (thanks to Nik)

fixed arity bug with "If" helpers for "If" that returns a function

given up disfruitful branch

explicit remove of lattice notation

moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy

moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy

dropped dead code

tuned isatest settings;

merged

moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax

tuned whitespace

tuned proof

prefer actual syntax categories;

avoid trait Addable, which is deprecated in scala-2.9.x; tuned;

streamlined abstract datatype;

tuned;

streamlined abstract datatype;

tuned -- avoid copy of empty value;

tuned;

streamlined abstract datatype, eliminating odd representation class;

tuned;

merged

make more simp rules respect int/bin distinction

make bool list functions respect int/bin distinction

merged;

tuned;

clarified Graph.restrict (formerly Graph.subgraph) based on public graph operations;

further graph operations from ML;

removed dead code;

directed graphs (in Scala);

make uses of bin_split respect int/bin distinction

remove lemma bin_cat_Pls, which doesn't respect int/bin distinction

make uses of constant bin_sc respect int/bin distinction

remove duplicate lemma bintrunc_Suc in favor of bintrunc.Suc

remove unused lemmas

simplify proofs

make uses of bin_sign respect int/bin distinction

removed unnecessary lemma zero_bintrunc

remove unnecessary lemmas

removed unnecessary constant bin_rl

remove duplication of lemmas bin_{rest,last}_BIT

remove lemmas Bit{0,1}_div2

simplify proof

deal with FIXMEs for linarith examples

CONTRIBUTORS

merged

tuned whitespace

tuned whitespace

adding documentation about find_unused_assms command and use_subtype option in the IsarRef

NEWS

adding some examples with find_unused_assms command

adding new command "find_unused_assms"

removing some unnecessary premises from Map theory

preliminarily switching quickcheck-narrowing off by default (probably it should only be invoked if concrete testing does not work)

generalizing inj_on_Int

moving Quickcheck's example to its own session

tuned proofs;

more robust visible_range: allow empty view;

misc tuning;

merged;

made SML/NJ happy;

tuned proofs;

merged

tuned proofs;

approximate Perspective.full within the bounds of the JVM;

misc tuning; more indentation;

invoke later to reduce chance of causing deadlock;

misc tuning; more indentation;

separate module for text status overview;

overview.delay_repaint: avoid wasting GUI cycles via update_delay; prefer delay_first for prover initiated events -- avoid indefinite delay;

tuned;

merged

merged

Fixed bugs: - set_env no longer modifies pfuns field in theory data record. Instead, a copy of this field is now contained in the env field. - add_type_def now checks whether type associated with SPARK enumeration type is really a datatype with no parameters. - check_pfuns_types now properly strips off prefixes of proof function names.

merged

subtype preprocessing in Quickcheck; adding option use_subtype; tuned

adding parsing of an optional predicate with quickcheck_generator command

updated generated files (cf. 8d51b375e926);

merged;

add missing lemmas to compute_div_mod

remove constant negateSnd in favor of 'apsnd uminus' (from Florian Haftmann)

avoid using constant Int.neg

renamed ex/Numeral.thy to ex/Numeral_Representation.thy