isabelle: Graph

updated TFF1 support
2011-12-07, by blanchet
updated Metis to 20110926 version
2011-12-07, by blanchet
remove unnecessary sublocale instantiations in HOL-Probability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space
2011-12-07, by hoelzl
remove mem_(c)ball_0 and centre_in_(c)ball from simpset, as rules mem_(c)ball always match instead
2011-12-05, by huffman
add cancellation simprocs for type enat
2011-12-07, by huffman
tuned
2011-12-07, by nipkow
increasing quickcheck's timeout in the example theory to avoid failures on the testing infrastructure
2011-12-06, by bulwahn
tuned proofs
2011-12-06, by hoelzl
added lemmas
2011-12-06, by nipkow
tuned proof
2011-12-05, by nipkow
real is better supported than real_of_nat, use it in the nat => ereal coercion
2011-12-05, by hoelzl
merged
2011-12-05, by kuncar
the note about morphisms moved in the description part
2011-12-05, by kuncar
updating documentation about quiet and verbose options in quickcheck
2011-12-05, by bulwahn
making the default behaviour of quickcheck a little bit less verbose;
2011-12-05, by bulwahn
adding verbose configuration to quickcheck
2011-12-05, by bulwahn
random reporting compilation returns if counterexample is genuine or potentially spurious, and takes genuine_only option as argument
2011-12-05, by bulwahn
the reporting random testing also returns if the counterexample is genuine or potentially spurious
2011-12-05, by bulwahn
exhaustive returns if a counterexample is genuine or potentially spurious in the presence of assumptions more correctly
2011-12-05, by bulwahn
inverted flag potential to genuine_only in the quickcheck narrowing Haskell code
2011-12-05, by bulwahn
NEWS
2011-12-05, by bulwahn
documenting the genuine_only option in quickcheck;
2011-12-05, by bulwahn
renaming potential flag to genuine_only flag with an inverse semantics
2011-12-05, by bulwahn
quickcheck narrowing continues searching after found a potentially spurious counterexample
2011-12-05, by bulwahn
outputing the potentially spurious counterexample and continue search
2011-12-05, by bulwahn
dynamic genuine_flag in compilation of random and exhaustive
2011-12-05, by bulwahn
indicating where the restart should occur; making safe_if dynamic
2011-12-05, by bulwahn
merged
2011-12-05, by nipkow
enforce parantheses around SKIP {_}
2011-12-05, by nipkow
adding genuine flag to predicate_compile_quickcheck and prolog_quickcheck (cf. 5e46c225370e);
2011-12-04, by bulwahn
merged
2011-12-04, by huffman
remove Library/Diagonalize.thy, because Library/Nat_Bijection.thy includes all the same functionality
2011-12-04, by huffman
missing dependency
2011-12-04, by nipkow
improved var names
2011-12-04, by nipkow
invariant holds before loop
2011-12-03, by nipkow
caret_range based on BreakIterator, which handles combined unicode characters as well;
2011-12-03, by wenzelm
misc tuning;
2011-12-02, by wenzelm
some localization;
2011-12-02, by wenzelm
eliminated some legacy operations;
2011-12-02, by wenzelm
more antiquotations;
2011-12-02, by wenzelm
tuned whitespace;
2011-12-02, by wenzelm
eliminated some legacy operations;
2011-12-02, by wenzelm
removed dead code, which has never been active in recorded history;
2011-12-02, by wenzelm
do not open ML structures;
2011-12-02, by wenzelm
tuned signature;
2011-12-02, by wenzelm
hide quickcheck constants Abs_cfun and Rep_cfun, to avoid clash with HOLCF
2011-12-02, by huffman
hiding internal constants and facts more properly
2011-12-01, by bulwahn
removing catch_match' now that catch_match is polymorphic
2011-12-01, by bulwahn
adapting exhaustive generators in record package
2011-12-01, by bulwahn
outputing if counterexample is potentially spurious or not
2011-12-01, by bulwahn
making catch_match polymorphic
2011-12-01, by bulwahn
compilations return genuine flag to quickcheck framework
2011-12-01, by bulwahn
extending quickcheck's result by the genuine flag
2011-12-01, by bulwahn
reporting random compilation also catches match exceptions internally
2011-12-01, by bulwahn
the narrowing also indicates if counterexample is potentially spurious
2011-12-01, by bulwahn
the simple exhaustive compilation also indicates if counterexample is potentially spurious;
2011-12-01, by bulwahn
quickcheck-random compilation also indicates if the counterexample is potentially spurious or not
2011-12-01, by bulwahn
changing the exhaustive generator signatures;
2011-12-01, by bulwahn
quickcheck's compilation returns if it is genuine counterexample or a counterexample due to a match exception
2011-12-01, by bulwahn
adding examples for quickcheck-random
2011-12-01, by bulwahn
removing exception handling now that is caught at some other point;
2011-12-01, by bulwahn
quickcheck random can also find potential counterexamples;
2011-12-01, by bulwahn
merged
2011-12-01, by wenzelm
merged IMP/Util into IMP/Vars
2011-12-01, by nipkow
use list theorems in Dining Cryptographers and Koepf Duermuth Countermeasure
2011-12-01, by hoelzl
cardinality of sets of lists
2011-12-01, by hoelzl
do not import examples Probability theory
2011-12-01, by hoelzl
moved theorems about distribution to the definition; removed oopsed-lemma
2011-12-01, by hoelzl
rename finite_prob_space.setsum_distribution, it collides with prob_space.setsum_distribution
2011-12-01, by hoelzl
remove duplicate theorem setsum_real_distribution
2011-12-01, by hoelzl
clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
2011-12-01, by wenzelm
updated Sledgehammer docs with new/renamed options
2011-12-01, by blanchet
added "minimize" option for more control over automatic minimization
2011-12-01, by blanchet
renamed "slicing" to "slice"
2011-12-01, by blanchet
tuning
2011-12-01, by blanchet
minor example tweak
2011-12-01, by blanchet
renamed inner syntax categories "num" to "num_token" and "xnum" to "xnum_token";
2011-12-01, by wenzelm
updated markup conforming to ML side;
2011-12-01, by wenzelm
discontinued obsolete datatype "alt_names";
2011-11-30, by wenzelm
misc tuning;
2011-11-30, by wenzelm
merged
2011-11-30, by wenzelm
removed outdated comment moved back and updated (at the direct request of Christian Urban)
2011-11-30, by kuncar
more stable introduction of the internally used unknown term
2011-11-30, by bulwahn
prefer typedef without alternative name;
2011-11-30, by wenzelm
prefer cpodef without extra definition;
2011-11-30, by wenzelm
prefer typedef without extra definition and alternative name;
2011-11-30, by wenzelm
tuned layout;
2011-11-30, by wenzelm
tuned header;
2011-11-30, by wenzelm
updated version information;
2011-11-30, by wenzelm
removed outdated comment
2011-11-30, by kuncar
adding examples for the potential counterexamples in the simple scheme
2011-11-30, by bulwahn
also potential counterexamples in the simple exhaustive testing in quickcheck
2011-11-30, by bulwahn
quickcheck does not show evaluation terms of equations if they are simply free variables to avoid duplicated output; tuned
2011-11-30, by bulwahn
adding more verbose messages to exhaustive quickcheck
2011-11-30, by bulwahn
quickcheck narrowing also shows potential counterexamples
2011-11-30, by bulwahn
adding a exception-safe term reification step in quickcheck; adding examples
2011-11-30, by bulwahn
quickcheck returns counterexamples that are potentially spurious due to underspecified code equations and match exceptions
2011-11-30, by bulwahn
adding parsing of potential configuration to quickcheck command
2011-11-30, by bulwahn
adding quickcheck's potential configuration
2011-11-30, by bulwahn
more conventional file name;
2011-11-29, by wenzelm
merged
2011-11-29, by wenzelm
updated documentation for the quotient package
2011-11-29, by kuncar
merged
2011-11-29, by kuncar
alternative names of morphisms in the definition of a quotient type can be specified
2011-11-29, by kuncar
adjusting antiquote_setup (cf. d83797ef0d2d)
2011-11-29, by bulwahn
clarified Time vs. Timing;
2011-11-29, by wenzelm
separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
2011-11-29, by wenzelm
clarified modules;
2011-11-29, by wenzelm
tuned proofs;
2011-11-29, by wenzelm
rearranged files;
2011-11-29, by wenzelm
merged
2011-11-29, by huffman
use HOL_basic_ss instead of HOL_ss for internal simproc proofs (cf. b36eedcd1633)
2011-11-28, by huffman
explicit indication of modules for independent Scala library;
2011-11-28, by wenzelm
separate module for concrete Isabelle markup;
2011-11-28, by wenzelm
renamed Isabelle_Markup to Isabelle_Rendering to emphasize its meaning and make room for Pure Isabelle_Markup module;
2011-11-28, by wenzelm
tuned signature (according to ML version);
2011-11-28, by wenzelm
merged
2011-11-28, by nipkow
Hide Product_Type.Times - too precious an identifier
2011-11-28, by nipkow
more antiquotations;
2011-11-28, by wenzelm
tuned messages;
2011-11-28, by wenzelm