2009-06-24 nipkow 2009-06-24 corrected and unified thm names
2009-06-23 haftmann 2009-06-23 merged
2009-06-23 haftmann 2009-06-23 merged
2009-06-23 haftmann 2009-06-23 Datatype.get_all
2009-06-23 haftmann 2009-06-23 corrected handling of free variables in arguments
2009-06-23 haftmann 2009-06-23 tuned proof
2009-06-23 haftmann 2009-06-23 tuned interfaces of datatype module
2009-06-23 haftmann 2009-06-23 add_datatypes does not yield particular rules any longer
2009-06-23 haftmann 2009-06-23 merged
2009-06-23 haftmann 2009-06-23 add_datatype interface yields type names and less rules
2009-06-23 wenzelm 2009-06-23 non-public representation;
2009-06-23 wenzelm 2009-06-23 fixed abbrev !! for \<And>;
2009-06-23 wenzelm 2009-06-23 merged
2009-06-23 haftmann 2009-06-23 merged
2009-06-23 haftmann 2009-06-23 simplified proof
2009-06-23 haftmann 2009-06-23 uniformly capitialized names for subdirectories
2009-06-23 haftmann 2009-06-23 renamed ioa to automaton
2009-06-23 haftmann 2009-06-23 renamed ioa to automaton
2009-06-23 haftmann 2009-06-23 dropped duplicated lemmas, tuned header
2009-06-23 haftmann 2009-06-23 NewNumberTheory depends on Algebra
2009-06-23 haftmann 2009-06-23 merged
2009-06-23 haftmann 2009-06-23 lemma funcset_id by Jeremy Avigad
2009-06-23 haftmann 2009-06-23 lemma finite_image_set by Jeremy Avigad
2009-06-23 nipkow 2009-06-23 merged
2009-06-23 nipkow 2009-06-23 new lemmas
2009-06-23 wenzelm 2009-06-23 tuned input: require longer symbol prefix; clarified result: no decode yet, single word with several completions;
2009-06-23 wenzelm 2009-06-23 moved string utilities to completion.scala; tuned;
2009-06-23 wenzelm 2009-06-23 Completion of symbols and keywords.
2009-06-23 wenzelm 2009-06-23 more precise implementation of trait methods -- oddly this seems to require copy/paste for +, ++; misc tuning;
2009-06-23 chaieb 2009-06-23 Added Library/Fraction_Field.thy: The fraction field of any integral domain
2009-06-23 nipkow 2009-06-23 merged
2009-06-23 nipkow 2009-06-23 fixed name
2009-06-22 wenzelm 2009-06-22 observe standard theory naming conventions; modernized headers;
2009-06-22 wenzelm 2009-06-22 end_timing: checked divisions with sane defaults;
2009-06-22 wenzelm 2009-06-22 eval: tuned input buffer and get_offset (which ran very hot, up to the point where AFP/FlyspeckTame would seemingly take forever);
2009-06-22 nipkow 2009-06-22 merged
2009-06-22 nipkow 2009-06-22 tuned FuncSet
2009-06-22 wenzelm 2009-06-22 Lexicon: removed unused max_entry;
2009-06-22 immler 2009-06-22 use results of relevance-filter to determine additional clauses; (needed for minimize to be able to prove the same problems as sledgehammer)
2009-06-22 immler 2009-06-22 export proof when exporting problemfile
2009-06-22 immler 2009-06-22 restructured external_prover
2009-06-22 immler 2009-06-22 corrected comments
2009-06-22 haftmann 2009-06-22 adapted to number theory switch
2009-06-22 haftmann 2009-06-22 merged
2009-06-21 haftmann 2009-06-21 code equation observes default sort constraints for types
2009-06-22 haftmann 2009-06-22 merged
2009-06-21 haftmann 2009-06-21 more precise computation of sort constraints
2009-06-21 haftmann 2009-06-21 merged
2009-06-21 haftmann 2009-06-21 merged
2009-06-21 haftmann 2009-06-21 merged
2009-06-21 haftmann 2009-06-21 discontinued ancient tradition to suffix certain ML module names with "_package"
2009-06-21 haftmann 2009-06-21 removed temporariy workarounds
2009-06-21 haftmann 2009-06-21 discontinued ancient tradition to suffix certain ML module names with "_package"
2009-06-21 haftmann 2009-06-21 simplified names of common datatype types
2009-06-21 haftmann 2009-06-21 more appropriate mk_typerep
2009-06-21 haftmann 2009-06-21 tuned interface
2009-06-21 nipkow 2009-06-21 new lemmas
2009-06-21 nipkow 2009-06-21 fixed NewNumberTheory deps
2009-06-21 nipkow 2009-06-21 fixed proof
2009-06-20 nipkow 2009-06-20 tuned