explicit locations for import_theory and setup_theory, for better user interface conformance

discontinued obsolete Library.foldl_map and Library.apply (NB: apply = fold I);

tuned;

tuned;

tuned;

canonical argument order for attribute application;

clarified terminology of raw protocol messages;

tuned;

tuned signature -- emphasize Isabelle_Process Input vs. Output;

explicit syslog_limit reduces danger of low-level message flooding; tuned;

retain original "uses" (again) -- still required for Thy_Load.use_file etc. in ML (notably for maintaining required/provided); tuned;

clarified scope of exception handlers;

relevant timing as in ML; more PIDE modules;

more fundamental pred-to-set conversions for range and domain by means of inductive_set

merged

tuned whitespace

tuned import

dropped dead code

terminate after first exception -- avoid syslog flooding;

avoid buffer loading overrun; tuned;

merged

collecting all axioms in a locale context in quickcheck; adding some verbose output;

choosing longer constant names in Quickcheck_Narrowing to reduce the chances of name clashes in Quickcheck-Narrowing

removing finiteness goals

adding finiteness of intervals on integer sets; adding another finiteness theorem for multisets

Symbol.encode header edits;

merged

tuned whitespace

more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)

Removal of obsolete ML bindings

more robust locking;

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