clarified special eol treatment and moved to gfx_range -- enables error messages at end of input, e.g. "prop PROP";

clarified command span: include trailing whitespace/comments and thus reduce number of ignored spans with associated transactions and states (factor 2); simplified signatures;

tuned

move test targets to test target

dropped images for importer sessions

dropped dead code

more accurate dependencies

tuned ML

dropped silly code

tuned

dropped dead code

actually add "the" Importer theory

avoid internal hol4 name references in generic importer code

generalized user-visible text

generalized attribute name

dropped dead theories

one unified Importer theory

added actual dependencies

import all importer theories in compatibility layer

merged;

dropped obsolete ROOT.ML

plugged in pre-existing theories appropriately

switch of target Import-HOL_Light-Imported: not operative at the moment

turn on quick and dirty in batch mode

tuned whitespace

file system structure separating HOL4 and HOL Light concerns

distribution of compatibility theories

formal infrastructure for import sessions

dropped dead code

tuned whitespace

spurious set/pred correction

explicit locations for import_theory and setup_theory, for better user interface conformance; spurious set/pred correction

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);