wenzelm [Sat, 04 Dec 2010 14:59:25 +0100] rev 40957
tuned @{datatype} using Syntax.pretty_priority (NB: postfix type application yields Syntax.max_pri, so arguments in prefix application require higher priority);
wenzelm [Sat, 04 Dec 2010 14:57:04 +0100] rev 40956
added Syntax.pretty_priority;
haftmann [Fri, 03 Dec 2010 22:40:26 +0100] rev 40955
merged
haftmann [Fri, 03 Dec 2010 14:46:58 +0100] rev 40954
conventional point-free characterization of rsp_fold
haftmann [Fri, 03 Dec 2010 14:39:15 +0100] rev 40953
replaced memb by existing List.member
haftmann [Fri, 03 Dec 2010 14:22:24 +0100] rev 40952
explicit type constraint;
streamlined notation
haftmann [Fri, 03 Dec 2010 22:39:34 +0100] rev 40951
tuned proposition
haftmann [Fri, 03 Dec 2010 22:34:20 +0100] rev 40950
lemma multiset_of_rev
haftmann [Fri, 03 Dec 2010 22:34:20 +0100] rev 40949
lemmas fold_remove1_split and fold_multiset_equiv
wenzelm [Fri, 03 Dec 2010 22:08:14 +0100] rev 40948
minor tuning for release;
wenzelm [Fri, 03 Dec 2010 21:34:54 +0100] rev 40947
source files are always encoded as UTF-8;
wenzelm [Fri, 03 Dec 2010 21:30:41 +0100] rev 40946
eliminated fragile HTML.with_charset -- always use utf-8;
wenzelm [Fri, 03 Dec 2010 20:38:58 +0100] rev 40945
recoded latin1 as utf8;
use textcomp for some text symbols where it appears appropriate;
wenzelm [Fri, 03 Dec 2010 20:26:57 +0100] rev 40944
removed old generated stuff;
removed DOS line endings;
wenzelm [Fri, 03 Dec 2010 20:02:57 +0100] rev 40943
comment;
blanchet [Fri, 03 Dec 2010 18:29:49 +0100] rev 40942
update documentation
blanchet [Fri, 03 Dec 2010 18:29:14 +0100] rev 40941
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet [Fri, 03 Dec 2010 18:27:21 +0100] rev 40940
export more information about available SMT solvers
wenzelm [Fri, 03 Dec 2010 17:59:13 +0100] rev 40939
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
traytel [Thu, 02 Dec 2010 21:48:36 +0100] rev 40938
use "fold_map" instead of "fold (fn .. => .. (ts @ [t], ..)) .."
wenzelm [Fri, 03 Dec 2010 17:31:27 +0100] rev 40937
updated generated file;
wenzelm [Fri, 03 Dec 2010 17:29:27 +0100] rev 40936
removed confusing comments (cf. 500171e7aa59);
wenzelm [Fri, 03 Dec 2010 17:18:41 +0100] rev 40935
merged
haftmann [Fri, 03 Dec 2010 14:00:55 +0100] rev 40934
removed outdated lint script
blanchet [Fri, 03 Dec 2010 10:43:09 +0100] rev 40933
merged
blanchet [Fri, 03 Dec 2010 10:28:39 +0100] rev 40932
compile
blanchet [Fri, 03 Dec 2010 09:55:45 +0100] rev 40931
run synchronous Auto Tools in parallel
krauss [Fri, 03 Dec 2010 10:17:55 +0100] rev 40930
really fixed comment (cf. 7abeb749ae99)
huffman [Fri, 03 Dec 2010 10:03:13 +0100] rev 40929
theorem names generated by the (rep_)datatype command now have mandatory qualifiers
krauss [Fri, 03 Dec 2010 10:03:10 +0100] rev 40928
eliminated unqualified accesses of datatype facts -- it seems like they all of them were unintended
bulwahn [Fri, 03 Dec 2010 09:58:32 +0100] rev 40927
NEWS
bulwahn [Fri, 03 Dec 2010 08:40:47 +0100] rev 40926
only instantiate type variable if there exists some in quickcheck
bulwahn [Fri, 03 Dec 2010 08:40:47 +0100] rev 40925
fixing comment in library
bulwahn [Fri, 03 Dec 2010 08:40:47 +0100] rev 40924
adapting predicate_compile_quickcheck
bulwahn [Fri, 03 Dec 2010 08:40:47 +0100] rev 40923
adding a nice definition of Id_on for quickcheck and nitpick
bulwahn [Fri, 03 Dec 2010 08:40:47 +0100] rev 40922
adding code equation for finiteness of finite types
bulwahn [Fri, 03 Dec 2010 08:40:47 +0100] rev 40921
improving sledgehammer_tactic and adding relevance filtering to the tactic
bulwahn [Fri, 03 Dec 2010 08:40:47 +0100] rev 40920
adapting mutabelle
bulwahn [Fri, 03 Dec 2010 08:40:47 +0100] rev 40919
adapting SML_Quickcheck to recent changes
bulwahn [Fri, 03 Dec 2010 08:40:47 +0100] rev 40918
explaining quickcheck testers in the documentation
bulwahn [Fri, 03 Dec 2010 08:40:47 +0100] rev 40917
adapting quickcheck examples
bulwahn [Fri, 03 Dec 2010 08:40:47 +0100] rev 40916
improving presentation of quickcheck reports
bulwahn [Fri, 03 Dec 2010 08:40:47 +0100] rev 40915
declaring quickcheck testers as default after their setup
bulwahn [Fri, 03 Dec 2010 08:40:47 +0100] rev 40914
activating construction of exhaustive testing combinators
bulwahn [Fri, 03 Dec 2010 08:40:47 +0100] rev 40913
renamed generator into exhaustive
bulwahn [Fri, 03 Dec 2010 08:40:47 +0100] rev 40912
checking if parameter is name of a tester which allows e.g. quickcheck[random]
bulwahn [Fri, 03 Dec 2010 08:40:47 +0100] rev 40911
moving iteration of tests to the testers in quickcheck
bulwahn [Fri, 03 Dec 2010 08:40:47 +0100] rev 40910
removed dead test_term_small function in quickcheck
bulwahn [Fri, 03 Dec 2010 08:40:47 +0100] rev 40909
renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn [Fri, 03 Dec 2010 08:40:47 +0100] rev 40908
adding configuration quickcheck_tester
bulwahn [Fri, 03 Dec 2010 08:40:47 +0100] rev 40907
adding smart quantifiers to exhaustive testing
bulwahn [Fri, 03 Dec 2010 08:40:47 +0100] rev 40906
adapting mutabelle
bulwahn [Fri, 03 Dec 2010 08:40:47 +0100] rev 40905
only handle TimeOut exception if used interactively
bulwahn [Fri, 03 Dec 2010 08:40:47 +0100] rev 40904
removed interrupt handling that violates Isabelle/ML exception model
bulwahn [Fri, 03 Dec 2010 08:40:47 +0100] rev 40903
corrected indentation
bulwahn [Fri, 03 Dec 2010 08:40:47 +0100] rev 40902
tuned
bulwahn [Fri, 03 Dec 2010 08:40:46 +0100] rev 40901
smallvalue_generator are defined quick via oracle or sound via function package
bulwahn [Fri, 03 Dec 2010 08:40:46 +0100] rev 40900
adding shorter output syntax for the finite types of quickcheck
bulwahn [Fri, 03 Dec 2010 08:40:46 +0100] rev 40899
improving readability of Smallcheck theory; adding constant orelse to improve performance of the function package
bulwahn [Fri, 03 Dec 2010 08:40:46 +0100] rev 40898
changed order of lemmas to overwrite the general code equation with the nbe-specific one