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;

tuned proof (via atp_minimized);

sort_strings (cf. Pure/library.ML);

clarified File.platform_path vs. File.shell_path; tuned;

exported File.shell_quote;

misc tuning and recovery of Isabelle coding style;

eliminated extraneous wrapping of public records; tuned;

tuned signature; tuned;

renamed functor HeapFun to Heap;

misc tuning and clarification;

structure ATP_Manager: eliminated slightly odd get/set operations in favour of Unsynchronized.ref; uniform interpretation of ATP_Manager.atps via ATP_Manager.get_atps;

modernized structure names;

show direct GC time (which is included in CPU time);

eliminated obsolete C/flip combinator;

added List.nth

tuned make parameters for sunbroy2;

accomodate old version of "tail", e.g. on sunbroy2;

settings for parallel experimental Poly/ML 5.3;

sharpened name

more explicit notion of canonized code equations

more explicit notion of canonized code equations

tuned whitespace

tuned whitespace

dropped Code_Printer prefix where feasible; fixed whitespace issues; more coherent terminology

merged

deactivated Datatype.distinct_simproc

dropped Datatype.distinct_simproc; tuned

order conjunctions to be printed without parentheses

approximation now fails earlier when using interval splitting; value [approximate] now supports bounded variables; renamed Var -> Atom for better readability

merged

added add_tyconames; tuned

merged

more appropriate abstraction over distinctness rules

merged

intro_base_names combinator

merged

dropped dist_ss