merged

explicit close_derivation

merged

map_range (and map_index) combinator

dropped Datatype.distinct_simproc

use Synchronized.assign to achieve actual immutable results;

support single-assigment variables -- based on magic RTS operations by David Matthews;

merged

fixed permissions -- this is a script, not an executable

inv_onto -> inv_into

renamed "nitpick_const_xxx" attributes to "nitpick_xxx" and "nitpick_ind_intros" to "nitpick_intros"

merged

fixed the "expect" mechanism of Refute in the face of timeouts

removed "nitpick_const_simp" attribute from Record's "simps"; Nitpick has its own notion of a record and doesn't need those.

merged

more accurate removal

merged

curried inter as canonical list operation (beware of argument order)

merged

proper handling of single literal case, added explicit exception, unfolding of distinct respects equal elements, made SML/NJ happy

Removed the hard-wired white list of theorems for sledgehammer

merged

Some new lemmas concerning sets

merged

curried union as canonical list operation

tuned ML import

removed old-style \ and \\ infixes

merged

dropped redundant gen_ prefix

replaced old_style infixes eq_set, subset, union, inter and variants by generic versions

find_theorems: better handling of abbreviations (by Timothy Bourke)

standardized basic operations on type option;

eliminated THENL -- use THEN RANGE; eliminated TRY' -- use TRY with op o; observe naming convention ctxt: Proof.context; tuned whitespace;

tuned;

fixed SML/NJ toplevel pp; tuned;

backpatching of structure Proof and ProofContext -- avoid odd aliases; renamed transfer_proof to raw_transfer; indicate firm naming conventions for theory, Proof.context, Context.generic;

tuned;

uniform use of Integer.min/max;

modernized session SET_Protocol;

modernized session Metis_Examples;

modernized session Isar_Examples;

tuned header;

more accurate dependencies for HOL-SMT, which is a session with image; misc cleanup;

removed unused map_force;

Removal of the unused atpset concept, the atp attribute and some related code.

additional schematic rules for Z3's rewrite rule

merged

added Hilbert_Choice section

merged

eliminated extraneous wrapping of public records, replaced simp_tac by best_tac (simplifier failed), less strict condition for rewrite (can also handle equations with single literal on left-hand side)

proper exceptions instead of unhandled partiality

footnote: inv via inv_onto

added inv_def for compatibility as a lemma

slightly less context-sensitive settings;

merged

corrected paths to certificates, added note how to re-generate the certificates

added proof reconstructon for Z3, added certificates for simpler re-checking of proofs (no need to invoke external solvers), added examples and certificates for all examples, removed Unsynchronized.ref (in smt_normalize.ML)

merged

merged

more accurate checkpoints

dropped lazy code equations

CONTRIBUTORS

always qualify NJ's old List.foldl/foldr in Isabelle/ML;

eliminated duplicate fold1 -- beware of argument order!

uniform use of Integer.add/mult/sum/prod;

Removed dead code in function mk_deftab.

Removed unneeded reference to inv_def.

Replaced inv by the_inv_onto.

Renamed inv to the_inv and turned it into an abbreviation (based on the_inv_onto).

fixed proof (cf. d1d4d7a08a66);

removed disjunctive group cancellation -- provers run independently; sledgehammer: kill earlier session, and removed obsolete max_atps; tuned;

tuned;

removed some unreferenced material; tuned;

merged

certificates for sos

merged

added sums of squares for standard deviation

merged

Inv -> inv_onto, inv abbr. inv_onto UNIV.

disable indent-tabs-mode in Proof General / Emacs;

merged

made SML/NJ happy;

Merged.

Finished revisions of locales tutorial.

Changed part of the examples to int.

Save current state of locales tutorial.

Observe order of declaration when printing registrations.

disable sunbroy2 for now;

tuned/moved divide_and_conquer';

tuned;

removed separate record_quick_and_dirty_sensitive;

simplified tactics; use proper SUBGOAL/CSUBGOAL;

eliminated old List.foldr and OldTerm operations; misc tuning;

removed unused names;

misc tuning and simplification;

less pervasive names;

operations of structure Skip_Proof (formerly SkipProof) no longer require quick_and_dirty mode;

Method.cheating: check quick_and_dirty here;

tuned;

Unsynchronized.set etc.;

indicate CRITICAL nature of various setmp combinators;

ISABELLE_TOOL;

tuned signature; observe coding conventions of this file;

merged

merged

added the_inv_onto

eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;

removed obsolete old goal command;

legacy Drule.standard is no longer pervasive;

explicitly qualify Drule.standard;

tuned white space;

local channels for tracing/debugging;

made SML/NJ happy;

sunbroy2: back to single-threaded mode for now -- deadlock in Poly/ML 5.3-SVN-900;

replaced String.concat by implode; replaced String.concatWith by space_implode; replaced (Seq.flat o Seq.map) by Seq.maps; replaced List.mapPartial by map_filter; replaced List.concat by flat; replaced (flat o map) by maps, which produces less garbage;

space_implode;

normalized aliases of Output operations;

eliminated slightly odd get/set operations in favour of Unsynchronized.ref; eliminated aliases of Output operations; print_cert: use warning for increased chance that the user actually sees the output; misc tuning and simplification;

natural argument order for prover; renamed atp_problem to problem; standard naming convention for the_system;

ATP_Manager.get_prover: canonical argument order; eliminated various aliases of existing operations, notably Output channels; tuned messages; misc tuning and clarification;