isabelle: Graph

replaced recdefs by funs
2009-06-27, by nipkow
tuned abbrevs;
2009-06-26, by wenzelm
lcm abs lemmas
2009-06-26, by nipkow
gcd abs lemmas
2009-06-26, by nipkow
NEWS updated
2009-06-25, by hoelzl
Improved computation of bounds and implemented interval splitting for 'approximation'.
2009-06-25, by hoelzl
Added new evaluator "approximate"
2009-06-08, by hoelzl
tuned
2009-06-15, by hoelzl
merged
2009-06-25, by haftmann
added List_Set and Code_Set theories
2009-06-25, by haftmann
merged
2009-06-25, by wenzelm
merged
2009-06-25, by haftmann
arbitrary farewell
2009-06-25, by haftmann
expand_path: handle parent (..) elements;
2009-06-25, by wenzelm
more stats;
2009-06-25, by wenzelm
merged
2009-06-25, by wenzelm
Streamlined code
2009-06-25, by nipkow
merged
2009-06-25, by nipkow
Cleaned up GCD
2009-06-25, by nipkow
renamed IsabelleProcess to Isabelle_Process;
2009-06-25, by wenzelm
renamed IsabelleSystem to Isabelle_System;
2009-06-25, by wenzelm
standard naming conventions for session and theories;
2009-06-24, by wenzelm
renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef -- Alice is no longer supported);
2009-06-24, by wenzelm
proper ML interface set_full_types;
2009-06-24, by wenzelm
Replaced Suc_remove by Suc_eq_plus1
2009-06-24, by nipkow
New ATP option: full types
2009-06-24, by nipkow
corrected and unified thm names
2009-06-24, by nipkow
merged
2009-06-23, by haftmann
merged
2009-06-23, by haftmann
Datatype.get_all
2009-06-23, by haftmann
corrected handling of free variables in arguments
2009-06-23, by haftmann
tuned proof
2009-06-23, by haftmann
tuned interfaces of datatype module
2009-06-23, by haftmann
add_datatypes does not yield particular rules any longer
2009-06-23, by haftmann
merged
2009-06-23, by haftmann
add_datatype interface yields type names and less rules
2009-06-23, by haftmann
non-public representation;
2009-06-23, by wenzelm
fixed abbrev !! for \<And>;
2009-06-23, by wenzelm
merged
2009-06-23, by wenzelm
merged
2009-06-23, by haftmann
simplified proof
2009-06-23, by haftmann
uniformly capitialized names for subdirectories
2009-06-23, by haftmann
renamed ioa to automaton
2009-06-23, by haftmann
renamed ioa to automaton
2009-06-23, by haftmann
dropped duplicated lemmas, tuned header
2009-06-23, by haftmann
NewNumberTheory depends on Algebra
2009-06-23, by haftmann
merged
2009-06-23, by haftmann
lemma funcset_id by Jeremy Avigad
2009-06-23, by haftmann
lemma finite_image_set by Jeremy Avigad
2009-06-23, by haftmann
merged
2009-06-23, by nipkow
new lemmas
2009-06-23, by nipkow
tuned input: require longer symbol prefix;
2009-06-23, by wenzelm
moved string utilities to completion.scala;
2009-06-23, by wenzelm
Completion of symbols and keywords.
2009-06-23, by wenzelm
more precise implementation of trait methods -- oddly this seems to require copy/paste for +, ++;
2009-06-23, by wenzelm
Added Library/Fraction_Field.thy: The fraction field of any integral
2009-06-23, by chaieb
merged
2009-06-23, by nipkow
fixed name
2009-06-23, by nipkow
observe standard theory naming conventions;
2009-06-22, by wenzelm
end_timing: checked divisions with sane defaults;
2009-06-22, by wenzelm
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, by wenzelm
merged
2009-06-22, by nipkow
tuned FuncSet
2009-06-22, by nipkow
Lexicon: removed unused max_entry;
2009-06-22, by wenzelm
use results of relevance-filter to determine additional clauses;
2009-06-22, by immler
export proof when exporting problemfile
2009-06-22, by immler
restructured external_prover
2009-06-22, by immler
corrected comments
2009-06-22, by immler
adapted to number theory switch
2009-06-22, by haftmann
merged
2009-06-22, by haftmann
code equation observes default sort constraints for types
2009-06-21, by haftmann
merged
2009-06-22, by haftmann
more precise computation of sort constraints
2009-06-21, by haftmann
merged
2009-06-21, by haftmann
merged
2009-06-21, by haftmann
merged
2009-06-21, by haftmann
discontinued ancient tradition to suffix certain ML module names with "_package"
2009-06-21, by haftmann
removed temporariy workarounds
2009-06-21, by haftmann
discontinued ancient tradition to suffix certain ML module names with "_package"
2009-06-21, by haftmann
simplified names of common datatype types
2009-06-21, by haftmann
more appropriate mk_typerep
2009-06-21, by haftmann
tuned interface
2009-06-21, by haftmann
new lemmas
2009-06-21, by nipkow
fixed NewNumberTheory deps
2009-06-21, by nipkow
fixed proof
2009-06-21, by nipkow
tuned
2009-06-20, by nipkow
added lemmas; tuned
2009-06-20, by nipkow
new lemmas and tuning
2009-06-20, by nipkow
merged
2009-06-19, by nipkow
Made Pi_I [simp]
2009-06-19, by nipkow
merged
2009-06-19, by haftmann
discontinued ancient tradition to suffix certain ML module names with "_package"
2009-06-19, by haftmann
more appropriate syntax for IML abstraction
2009-06-19, by haftmann
discontinued ancient tradition to suffix certain ML module names with "_package"
2009-06-19, by haftmann
merged
2009-06-19, by nipkow
tuned
2009-06-19, by nipkow
NewNumberTheory
2009-06-19, by nipkow
Added NewNumberTheory by Jeremy Avigad
2009-06-19, by nipkow
fixed thm name
2009-06-19, by nipkow
fix name clash with old/new prime libraries
2009-06-18, by huffman
merged
2009-06-18, by huffman
update to work with new GCD library
2009-06-18, by huffman
generalized less_Suc_induct
2009-06-18, by krauss
merged
2009-06-18, by wenzelm
update ex/Sqrt.thy to use new GCD library
2009-06-18, by huffman
update to use new GCD library
2009-06-18, by huffman
merged
2009-06-18, by huffman
more [code del] declarations
2009-06-18, by huffman
add NatTransfer.thy, needed for new GCD library
2009-06-17, by huffman
merged
2009-06-17, by huffman
new GCD library, courtesy of Jeremy Avigad
2009-06-17, by huffman
replaced java Properties by pure property lists;
2009-06-18, by wenzelm
environment: keep original HOME and PATH (required for Cygwin integrity);
2009-06-18, by wenzelm
added toString;
2009-06-18, by wenzelm
jar: jvmpath wrapper (requires bash);
2009-06-18, by wenzelm
subSequence: bounds checking;
2009-06-18, by wenzelm
added reverse CharSequence;
2009-06-18, by wenzelm
merged
2009-06-18, by haftmann
uncheck is liberal wrt. semityped terms
2009-06-17, by haftmann
stripped dead comment
2009-06-17, by haftmann
skip_proof where appropriate
2009-06-17, by haftmann
more robust poly startup, by restricting heap size (otherwise it fails on very large memory);
2009-06-17, by wenzelm
merged
2009-06-17, by wenzelm
end_timing: actually display GC percentage, not factor;
2009-06-17, by wenzelm
merged
2009-06-17, by wenzelm
Polishing the English
2009-06-17, by paulson
rtrancl lemmas
2009-06-17, by nipkow
made SML/NJ happy;
2009-06-17, by wenzelm
usedir: internal timing option;
2009-06-17, by wenzelm
more detailed start_timing/end_timing;
2009-06-17, by wenzelm
more detailed start_timing/end_timing (in timing.ML);
2009-06-17, by wenzelm
removed obsolete time accumulator (better use Toplevel.profiling);
2009-06-17, by wenzelm
minor tuning according to Isabelle/ML conventions;
2009-06-17, by wenzelm
back to polyml-5.2.1;
2009-06-17, by wenzelm
corrected some issues
2009-06-17, by haftmann
refined section concerning classes
2009-06-17, by haftmann
reworked section on type classes
2009-06-17, by haftmann
merged
2009-06-17, by haftmann
reworked section on type classes
2009-06-17, by haftmann
updated table of overloaded constants
2009-06-17, by haftmann
more precise dependencies
2009-06-17, by haftmann
fixed grammar
2009-06-17, by haftmann
obey SML syntax even more closely
2009-06-17, by haftmann
merged
2009-06-17, by haftmann
obey SML syntax more closely
2009-06-17, by haftmann
datatype packages: record datatype_config for configuration flags; less verbose signatures
2009-06-17, by haftmann
merged
2009-06-16, by haftmann
ignore in-situ contrib symlinks
2009-06-16, by haftmann
datatype packages: record datatype_config for configuration flags; less verbose signatures
2009-06-16, by haftmann
dropped ID
2009-06-16, by haftmann
denominator should not be zero
2009-06-16, by haftmann
tuned brackets for let expressions etc.
2009-06-16, by haftmann
merged
2009-06-16, by huffman
smult_dvd lemmas; polynomial gcd
2009-06-16, by huffman
generalize lemmas dvd_mod and dvd_mod_iff to class semiring_div
2009-06-15, by huffman
move lemma div_power into semiring_div context; class ring_div inherits from idom
2009-06-15, by huffman
generalize many constants and lemmas from Convex_Euclidean_Space
2009-06-13, by huffman
generalize lemma connected_real_lemma
2009-06-13, by huffman
generalize lemmas
2009-06-13, by huffman
replace uses of (bi)linear with bounded_(bi)linear
2009-06-13, by huffman
new continuous/vimage lemmas; cleaned up proofs
2009-06-13, by huffman
generalize constants netlimit and continuous
2009-06-13, by huffman
generalize lemma Lim_unique to t2_space
2009-06-13, by huffman
less ambitious ML_OPTIONS;
2009-06-16, by wenzelm
another attempt to get a reduced at-sml-dev-e test;
2009-06-16, by wenzelm
added names, abbrevs;
2009-06-16, by wenzelm
added completions;
2009-06-16, by wenzelm
reorganized and abstracted version, via Set trait;
2009-06-16, by wenzelm
Efficient scanning of literals.
2009-06-16, by wenzelm
merged
2009-06-15, by wenzelm
override toplevel "use" functions last;
2009-06-15, by wenzelm
made SML/NJ happy;
2009-06-15, by wenzelm
Quickcheck.random
2009-06-15, by haftmann
authentic syntax for Pow and image
2009-06-15, by haftmann
permissive code attribute; all_eqns
2009-06-15, by haftmann
hide constant Quickcheck.random
2009-06-15, by haftmann
more parallel stats;
2009-06-15, by wenzelm
merged
2009-06-15, by wenzelm
made SML/NJ happy
2009-06-15, by haftmann
skip_proof not operative here
2009-06-15, by haftmann
where there is nothing, nothing can be hidden
2009-06-15, by haftmann
axclass command now legacy
2009-06-14, by haftmann
using skip_proof where appropriate
2009-06-14, by haftmann
dropped select_default
2009-06-14, by haftmann
removed obsolete depend, add_job_acyclic;
2009-06-14, by wenzelm
simplified join: do not record dependencies (which are slow, but were only required for dequeue_towards);
2009-06-14, by wenzelm
back to default -M max, with more robust interpretation of corresponding max_threads value;
2009-06-14, by wenzelm
merged
2009-06-14, by haftmann
dropped diagnostic handles
2009-06-14, by haftmann
merged
2009-06-14, by haftmann
merged
2009-06-13, by haftmann
using SkipProof where appropriate
2009-06-13, by haftmann
quickcheck using generic code generator
2009-06-13, by haftmann
quickcheck generators for datatypes with functions
2009-06-13, by haftmann
more convenient signature for random_fun_lift
2009-06-13, by haftmann
improved correctness of get_first (boundary check);
2009-06-14, by wenzelm
more isatest platforms;
2009-06-14, by wenzelm
tuned join: produce less garbage while waiting;
2009-06-14, by wenzelm
improved get_first: check boundary before entering subtrees;
2009-06-13, by wenzelm
simplified join_results: no longer work "towards" deps, which simplifies task queue management and maintains strict bottom up discipline (without "transfer of priority" to required futures);
2009-06-13, by wenzelm
native get_first, with optional boundary;
2009-06-13, by wenzelm
moved at-mac-poly-5.1-para back to macbroy6, for continous performance figures;
2009-06-13, by wenzelm
merged
2009-06-13, by haftmann
merged
2009-06-11, by haftmann
merged
2009-06-11, by haftmann
explicit instantiation yields considerable speedup
2009-06-11, by haftmann
separate directory for datatype package
2009-06-10, by haftmann
tuned whitespace
2009-06-10, by haftmann
correct check for instantiatability
2009-06-10, by haftmann
tuned order
2009-06-10, by haftmann
merged
2009-06-10, by haftmann
separate directory for datatype package
2009-06-10, by haftmann
separate directory for datatype package
2009-06-10, by haftmann
revised interpretation combinator for datatype constructions
2009-06-10, by haftmann
tuned header
2009-06-10, by haftmann
merged
2009-06-10, by haftmann
merged
2009-06-09, by haftmann
tuned make/map/merge combinators
2009-06-09, by haftmann
corrected printing of record labels
2009-06-09, by haftmann
tuned author list
2009-06-09, by haftmann
tuned whitespace
2009-06-09, by haftmann
first running version of qc generators for datatypes
2009-06-09, by haftmann
less brackets
2009-06-09, by haftmann
merged
2009-06-13, by huffman
generalize lemmas about inner
2009-06-12, by huffman
replace all occurrences of dot at type real^'n with inner
2009-06-12, by huffman
declare inner_add, inner_diff [algebra_simps]; declare inner_scaleR [simp]
2009-06-12, by huffman
avoid using vec1 in continuity lemmas
2009-06-12, by huffman
add lemma tendsto_setsum
2009-06-12, by huffman
remove simp add: norm_scaleR
2009-06-12, by huffman
declare norm_scaleR [simp]; declare scaleR_cancel lemmas [simp]
2009-06-12, by huffman
replace all occurrences of 'op *s' at type real^'n with scaleR
2009-06-12, by huffman
proper ISABELLE_HOME_USER;
2009-06-13, by wenzelm
eliminated obsolete CVS2CL;
2009-06-12, by wenzelm
eliminated cvs ids;
2009-06-12, by wenzelm
more isatests;
2009-06-12, by wenzelm
added cases to code_pred command
2009-06-12, by bulwahn
merged
2009-06-12, by bulwahn
merged
2009-06-12, by bulwahn
added lemma
2009-06-11, by bulwahn