2011-03-20 wenzelm 2011-03-20 modernized specifications;
2011-03-20 wenzelm 2011-03-20 dropped unused structure aliases;
2011-03-20 wenzelm 2011-03-20 tuned;
2011-03-20 wenzelm 2011-03-20 NEWS: structure Timing provides various operations for timing;
2011-03-20 wenzelm 2011-03-20 simplified various cpu_time clones (!): eliminated odd Exn.capture/Exn.release (no need to "stop" timing);
2011-03-20 wenzelm 2011-03-20 pure Timing.timing, without any exception handling; clarified cond_timeit: propagate interrupt without side-effect;
2011-03-20 wenzelm 2011-03-20 structure Timing: covers former start_timing/end_timing and Output.timeit etc; explicit Timing.message function; eliminated Output.timing flag, cf. Toplevel.timing; tuned;
2011-03-20 wenzelm 2011-03-20 pervasive cond_timeit;
2011-03-20 wenzelm 2011-03-20 eliminated dead code;
2011-03-20 wenzelm 2011-03-20 parallel preparation of document variants, within separate directories;
2011-03-20 wenzelm 2011-03-20 Present.init/finish/no_document are not thread-safe -- eliminated futile CRITICAL sections; tuned;
2011-03-20 wenzelm 2011-03-20 eliminated redundant doc_prefix1; tuned;
2011-03-20 wenzelm 2011-03-20 renamed doc_prefix2 to dump_prefix;
2011-03-20 wenzelm 2011-03-20 tuned;
2011-03-20 wenzelm 2011-03-20 tuned terminology for document variants;
2011-03-20 wenzelm 2011-03-20 replaced File.check by specific File.check_file, File.check_dir; clarified File.full_path -- include parts of former Thy_Load.get_file; simplified Thy_Load.check_file -- do not read/digest yet; merged Thy_Load.check_thy/deps_thy -- always read text and parse header; clarified Thy_Header.read -- NB: partial Path.explode outside of args parser combinator; Thy_Info.check_deps etc.: File.read exactly once;
2011-03-20 wenzelm 2011-03-20 tuned;
2011-03-19 blanchet 2011-03-19 preencode value of "need" selectors in Kodkod bounds as an optimization
2011-03-19 blanchet 2011-03-19 ignore "need" axioms for "nat"-like types
2011-03-18 blanchet 2011-03-18 added "simp:", "intro:", and "elim:" to "try" command
2011-03-18 blanchet 2011-03-18 optimize Kodkod axioms further w.r.t. "need" option
2011-03-18 blanchet 2011-03-18 optimize Kodkod bounds of nat-like datatypes
2011-03-18 blanchet 2011-03-18 more optimizations of bounds for "need"
2011-03-18 blanchet 2011-03-18 optimize Kodkod bounds when "need" is specified
2011-03-18 blanchet 2011-03-18 always destroy constructor patterns, since this seems to be always useful
2011-03-17 blanchet 2011-03-17 reintroduced "show_skolems" option -- useful when too many Skolems are displayed
2011-03-17 blanchet 2011-03-17 reword Nitpick's wording concerning potential counterexamples
2011-03-17 blanchet 2011-03-17 prevent an exception if "card" is empty (e.g., "nitpick [card]")
2011-03-17 blanchet 2011-03-17 add option to function to keep trivial ATP formulas, needed for some experiments
2011-03-17 blanchet 2011-03-17 add option to relevance filter's "all_facts" function to really get all facts (needed for some experiments)
2011-03-17 nipkow 2011-03-17 tuned lemma
2011-03-16 nipkow 2011-03-16 added lemmas
2011-03-15 nipkow 2011-03-15 added lemma
2011-03-15 blanchet 2011-03-15 support non-ground "need" values
2011-03-15 wenzelm 2011-03-15 recover Isabelle symlink for public distribution, notably website;
2011-03-14 wenzelm 2011-03-14 standardized headers;
2011-03-14 hoelzl 2011-03-14 merged
2011-03-14 hoelzl 2011-03-14 reworked Probability theory: measures are not type restricted to positive extended reals
2011-03-14 hoelzl 2011-03-14 split Extended_Reals into parts for Library and Multivariate_Analysis
2011-03-14 hoelzl 2011-03-14 lemmas about addition, SUP on countable sets and infinite sums for extreal
2011-03-14 hoelzl 2011-03-14 add infinite sums and power on extreal
2011-03-14 hoelzl 2011-03-14 introduce setsum on extreal
2011-03-14 hoelzl 2011-03-14 use abs_extreal
2011-03-14 hoelzl 2011-03-14 simplified definition of open_extreal
2011-03-14 hoelzl 2011-03-14 use case_product for extrel[2,3]_cases
2011-03-14 hoelzl 2011-03-14 add Extended_Reals from AFP/Lower_Semicontinuous
2011-03-14 hoelzl 2011-03-14 add lemmas for monotone sequences
2011-03-14 hoelzl 2011-03-14 add lemmas for SUP and INF
2011-03-14 hoelzl 2011-03-14 generalize infinite sums
2011-03-14 hoelzl 2011-03-14 moved t2_spaces to HOL image
2011-03-14 wenzelm 2011-03-14 example settings for ISABELLE_GHC, ISABELLE_OCAML, ISABELLE_SWIPL;
2011-03-14 wenzelm 2011-03-14 isatest: fresh copy of settings avoids odd cumulative environment;
2011-03-14 bulwahn 2011-03-14 tuned exhaustive_generators
2011-03-14 bulwahn 2011-03-14 removing definition of cons0; hiding constants in Quickcheck_Narrowing
2011-03-14 bulwahn 2011-03-14 tuned subsubsection names in Quickcheck_Narrowing
2011-03-14 bulwahn 2011-03-14 tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
2011-03-14 bulwahn 2011-03-14 correcting names in Narrowing_Engine and example theory for Quickcheck_Narrowing
2011-03-14 bulwahn 2011-03-14 renaming series and serial to narrowing in Quickcheck_Narrowing
2011-03-13 wenzelm 2011-03-13 eliminated Bali.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 9b19cbb0af28;
2011-03-13 wenzelm 2011-03-13 tuned headers;