isabelle: Graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -30000 -10000 -3000 -1000 -112 +112 +1000 +3000 +10000 +30000 tip

merged
2009-10-22, by boehmes
fixed permissions -- this is a script, not an executable
2009-10-22, by boehmes
inv_onto -> inv_into
2009-10-22, by nipkow
renamed "nitpick_const_xxx" attributes to "nitpick_xxx" and "nitpick_ind_intros" to "nitpick_intros"
2009-10-21, by blanchet
merged
2009-10-21, by blanchet
fixed the "expect" mechanism of Refute in the face of timeouts
2009-10-21, by blanchet
removed "nitpick_const_simp" attribute from Record's "simps";
2009-10-21, by blanchet
merged
2009-10-21, by haftmann
more accurate removal
2009-10-21, by haftmann
merged
2009-10-21, by haftmann
curried inter as canonical list operation (beware of argument order)
2009-10-21, by haftmann
merged
2009-10-21, by boehmes
proper handling of single literal case,
2009-10-21, by boehmes
Removed the hard-wired white list of theorems for sledgehammer
2009-10-21, by paulson
merged
2009-10-21, by paulson
Some new lemmas concerning sets
2009-10-20, by paulson
merged
2009-10-21, by haftmann
curried union as canonical list operation
2009-10-21, by haftmann
tuned ML import
2009-10-21, by haftmann
removed old-style \ and \\ infixes
2009-10-21, by haftmann
merged
2009-10-21, by haftmann
dropped redundant gen_ prefix
2009-10-21, by haftmann
replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
2009-10-20, by haftmann
find_theorems: better handling of abbreviations (by Timothy Bourke)
2009-10-21, by kleing
standardized basic operations on type option;
2009-10-21, by wenzelm
eliminated THENL -- use THEN RANGE;
2009-10-20, by wenzelm
tuned;
2009-10-20, by wenzelm
fixed SML/NJ toplevel pp;
2009-10-20, by wenzelm
backpatching of structure Proof and ProofContext -- avoid odd aliases;
2009-10-20, by wenzelm
tuned;
2009-10-20, by wenzelm
uniform use of Integer.min/max;
2009-10-20, by wenzelm
modernized session SET_Protocol;
2009-10-20, by wenzelm
modernized session Metis_Examples;
2009-10-20, by wenzelm
modernized session Isar_Examples;
2009-10-20, by wenzelm
tuned header;
2009-10-20, by wenzelm
more accurate dependencies for HOL-SMT, which is a session with image;
2009-10-20, by wenzelm
removed unused map_force;
2009-10-20, by wenzelm
Removal of the unused atpset concept, the atp attribute and some related code.
2009-10-20, by paulson
additional schematic rules for Z3's rewrite rule
2009-10-20, by boehmes
merged
2009-10-20, by nipkow
added Hilbert_Choice section
2009-10-20, by nipkow
merged
2009-10-20, by boehmes
eliminated extraneous wrapping of public records,
2009-10-20, by boehmes
proper exceptions instead of unhandled partiality
2009-10-20, by boehmes
footnote: inv via inv_onto
2009-10-20, by nipkow
added inv_def for compatibility as a lemma
2009-10-20, by nipkow
slightly less context-sensitive settings;
2009-10-20, by wenzelm
merged
2009-10-20, by wenzelm
corrected paths to certificates,
2009-10-20, by boehmes
added proof reconstructon for Z3,
2009-10-20, by boehmes
merged
2009-10-20, by wenzelm
merged
2009-10-20, by haftmann
more accurate checkpoints
2009-10-20, by haftmann
dropped lazy code equations
2009-10-19, by haftmann
CONTRIBUTORS
2009-10-19, by haftmann
always qualify NJ's old List.foldl/foldr in Isabelle/ML;
2009-10-19, by wenzelm
eliminated duplicate fold1 -- beware of argument order!
2009-10-19, by wenzelm
uniform use of Integer.add/mult/sum/prod;
2009-10-19, by wenzelm
Removed dead code in function mk_deftab.
2009-10-19, by berghofe
Removed unneeded reference to inv_def.
2009-10-19, by berghofe
Replaced inv by the_inv_onto.
2009-10-19, by berghofe
Renamed inv to the_inv and turned it into an abbreviation (based on the_inv_onto).
2009-10-19, by berghofe
fixed proof (cf. d1d4d7a08a66);
2009-10-18, by wenzelm
removed disjunctive group cancellation -- provers run independently;
2009-10-18, by wenzelm
tuned;
2009-10-18, by wenzelm
removed some unreferenced material;
2009-10-18, by wenzelm
merged
2009-10-18, by nipkow
certificates for sos
2009-10-18, by nipkow
merged
2009-10-18, by nipkow
added sums of squares for standard deviation
2009-10-18, by nipkow
merged
2009-10-18, by nipkow
Inv -> inv_onto, inv abbr. inv_onto UNIV.
2009-10-18, by nipkow
disable indent-tabs-mode in Proof General / Emacs;
2009-10-18, by wenzelm
merged
2009-10-17, by wenzelm
made SML/NJ happy;
2009-10-17, by wenzelm
Merged.
2009-10-17, by ballarin
Finished revisions of locales tutorial.
2009-10-17, by ballarin
Changed part of the examples to int.
2009-10-15, by ballarin
Save current state of locales tutorial.
2009-10-15, by ballarin
Observe order of declaration when printing registrations.
2009-10-15, by ballarin
disable sunbroy2 for now;
2009-10-17, by wenzelm
tuned/moved divide_and_conquer';
2009-10-17, by wenzelm
tuned;
2009-10-17, by wenzelm
removed separate record_quick_and_dirty_sensitive;
2009-10-17, by wenzelm
simplified tactics;
2009-10-17, by wenzelm
eliminated old List.foldr and OldTerm operations;
2009-10-17, by wenzelm
removed unused names;
2009-10-17, by wenzelm
misc tuning and simplification;
2009-10-17, by wenzelm
less pervasive names;
2009-10-17, by wenzelm
operations of structure Skip_Proof (formerly SkipProof) no longer require quick_and_dirty mode;
2009-10-17, by wenzelm
Method.cheating: check quick_and_dirty here;
2009-10-17, by wenzelm
tuned;
2009-10-17, by wenzelm
Unsynchronized.set etc.;
2009-10-17, by wenzelm
indicate CRITICAL nature of various setmp combinators;
2009-10-17, by wenzelm
ISABELLE_TOOL;
2009-10-17, by wenzelm
tuned signature;
2009-10-17, by wenzelm
merged
2009-10-17, by wenzelm
merged
2009-10-17, by nipkow
added the_inv_onto
2009-10-17, by nipkow
eliminated hard tabulators, guessing at each author's individual tab-width;
2009-10-17, by wenzelm
removed obsolete old goal command;
2009-10-17, by wenzelm
legacy Drule.standard is no longer pervasive;
2009-10-17, by wenzelm
explicitly qualify Drule.standard;
2009-10-17, by wenzelm
tuned white space;
2009-10-16, by wenzelm
local channels for tracing/debugging;
2009-10-16, by wenzelm
made SML/NJ happy;
2009-10-16, by wenzelm
sunbroy2: back to single-threaded mode for now -- deadlock in Poly/ML 5.3-SVN-900;
2009-10-15, by wenzelm
replaced String.concat by implode;
2009-10-15, by wenzelm
space_implode;
2009-10-15, by wenzelm
normalized aliases of Output operations;
2009-10-15, by wenzelm
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
2009-10-15, by wenzelm
natural argument order for prover;
2009-10-15, by wenzelm