2009-10-20 haftmann 2009-10-20 replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
2009-10-21 kleing 2009-10-21 find_theorems: better handling of abbreviations (by Timothy Bourke)
2009-10-21 wenzelm 2009-10-21 standardized basic operations on type option;
2009-10-20 wenzelm 2009-10-20 eliminated THENL -- use THEN RANGE; eliminated TRY' -- use TRY with op o; observe naming convention ctxt: Proof.context; tuned whitespace;
2009-10-20 wenzelm 2009-10-20 tuned;
2009-10-20 wenzelm 2009-10-20 fixed SML/NJ toplevel pp; tuned;
2009-10-20 wenzelm 2009-10-20 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;
2009-10-20 wenzelm 2009-10-20 tuned;
2009-10-20 wenzelm 2009-10-20 uniform use of Integer.min/max;
2009-10-20 wenzelm 2009-10-20 modernized session SET_Protocol;
2009-10-20 wenzelm 2009-10-20 modernized session Metis_Examples;
2009-10-20 wenzelm 2009-10-20 modernized session Isar_Examples;
2009-10-20 wenzelm 2009-10-20 tuned header;
2009-10-20 wenzelm 2009-10-20 more accurate dependencies for HOL-SMT, which is a session with image; misc cleanup;
2009-10-20 wenzelm 2009-10-20 removed unused map_force;
2009-10-20 paulson 2009-10-20 Removal of the unused atpset concept, the atp attribute and some related code.
2009-10-20 boehmes 2009-10-20 additional schematic rules for Z3's rewrite rule
2009-10-20 nipkow 2009-10-20 merged
2009-10-20 nipkow 2009-10-20 added Hilbert_Choice section
2009-10-20 boehmes 2009-10-20 merged
2009-10-20 boehmes 2009-10-20 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)
2009-10-20 boehmes 2009-10-20 proper exceptions instead of unhandled partiality
2009-10-20 nipkow 2009-10-20 footnote: inv via inv_onto
2009-10-20 nipkow 2009-10-20 added inv_def for compatibility as a lemma
2009-10-20 wenzelm 2009-10-20 slightly less context-sensitive settings;
2009-10-20 wenzelm 2009-10-20 merged
2009-10-20 boehmes 2009-10-20 corrected paths to certificates, added note how to re-generate the certificates
2009-10-20 boehmes 2009-10-20 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)
2009-10-20 wenzelm 2009-10-20 merged
2009-10-20 haftmann 2009-10-20 merged
2009-10-20 haftmann 2009-10-20 more accurate checkpoints
2009-10-19 haftmann 2009-10-19 dropped lazy code equations
2009-10-19 haftmann 2009-10-19 CONTRIBUTORS
2009-10-19 wenzelm 2009-10-19 always qualify NJ's old List.foldl/foldr in Isabelle/ML;
2009-10-19 wenzelm 2009-10-19 eliminated duplicate fold1 -- beware of argument order!
2009-10-19 wenzelm 2009-10-19 uniform use of Integer.add/mult/sum/prod;
2009-10-19 berghofe 2009-10-19 Removed dead code in function mk_deftab.
2009-10-19 berghofe 2009-10-19 Removed unneeded reference to inv_def.
2009-10-19 berghofe 2009-10-19 Replaced inv by the_inv_onto.
2009-10-19 berghofe 2009-10-19 Renamed inv to the_inv and turned it into an abbreviation (based on the_inv_onto).
2009-10-18 wenzelm 2009-10-18 fixed proof (cf. d1d4d7a08a66);
2009-10-18 wenzelm 2009-10-18 removed disjunctive group cancellation -- provers run independently; sledgehammer: kill earlier session, and removed obsolete max_atps; tuned;
2009-10-18 wenzelm 2009-10-18 tuned;
2009-10-18 wenzelm 2009-10-18 removed some unreferenced material; tuned;
2009-10-18 nipkow 2009-10-18 merged
2009-10-18 nipkow 2009-10-18 certificates for sos
2009-10-18 nipkow 2009-10-18 merged
2009-10-18 nipkow 2009-10-18 added sums of squares for standard deviation
2009-10-18 nipkow 2009-10-18 merged
2009-10-18 nipkow 2009-10-18 Inv -> inv_onto, inv abbr. inv_onto UNIV.
2009-10-18 wenzelm 2009-10-18 disable indent-tabs-mode in Proof General / Emacs;
2009-10-17 wenzelm 2009-10-17 merged
2009-10-17 wenzelm 2009-10-17 made SML/NJ happy;
2009-10-17 ballarin 2009-10-17 Merged.
2009-10-17 ballarin 2009-10-17 Finished revisions of locales tutorial.
2009-10-15 ballarin 2009-10-15 Changed part of the examples to int.
2009-10-15 ballarin 2009-10-15 Save current state of locales tutorial.
2009-10-15 ballarin 2009-10-15 Observe order of declaration when printing registrations.
2009-10-17 wenzelm 2009-10-17 disable sunbroy2 for now;
2009-10-17 wenzelm 2009-10-17 tuned/moved divide_and_conquer';