kuncar [Tue, 13 Dec 2011 14:04:20 +0100] rev 45826
support phantom types as quotient types
wenzelm [Mon, 12 Dec 2011 23:06:41 +0100] rev 45825
merged
nipkow [Mon, 12 Dec 2011 20:28:34 +0100] rev 45824
merged
nipkow [Mon, 12 Dec 2011 20:28:19 +0100] rev 45823
tuned
wenzelm [Mon, 12 Dec 2011 23:05:21 +0100] rev 45822
datatype dtyp with explicit sort information;
tuned messages;
wenzelm [Mon, 12 Dec 2011 20:55:57 +0100] rev 45821
tuned;
wenzelm [Mon, 12 Dec 2011 19:47:50 +0100] rev 45820
updated generated file;
bulwahn [Mon, 12 Dec 2011 17:22:48 +0100] rev 45819
tuned quickcheck's response
bulwahn [Mon, 12 Dec 2011 13:45:54 +0100] rev 45818
hiding constants and facts in the Quickcheck_Exhaustive and Quickcheck_Narrowing theory;
huffman [Mon, 12 Dec 2011 12:03:34 +0100] rev 45817
merged
huffman [Mon, 12 Dec 2011 08:19:37 +0100] rev 45816
replace more uses of 'lemmas' with explicit 'lemma';
replace uses of 'simplified' attribute with 'unfolded';
remove unused intermediate lemmas.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 12 Dec 2011 15:32:54 +0900] rev 45815
Add Quotient_Rat: an example of using the quotient package with partial equivalence relations, defining rational numbers.
huffman [Sun, 11 Dec 2011 21:57:22 +0100] rev 45814
fix spelling
huffman [Sun, 11 Dec 2011 21:54:20 +0100] rev 45813
fix spelling
nipkow [Sun, 11 Dec 2011 18:22:06 +0100] rev 45812
added IMP/Live_True.thy
huffman [Sun, 11 Dec 2011 09:55:57 +0100] rev 45811
replace many uses of 'lemmas' with 'lemma';
remove many unused intermediate lemmas.
huffman [Sat, 10 Dec 2011 22:00:42 +0100] rev 45810
prove class instances without extra lemmas
huffman [Sat, 10 Dec 2011 21:48:16 +0100] rev 45809
finite class instance for word type; remove unused lemmas
huffman [Sat, 10 Dec 2011 21:07:59 +0100] rev 45808
remove unused lemmas
huffman [Sat, 10 Dec 2011 16:24:22 +0100] rev 45807
generalize some lemmas
huffman [Sat, 10 Dec 2011 13:00:58 +0100] rev 45806
merged
huffman [Sat, 10 Dec 2011 08:29:19 +0100] rev 45805
tidied Word.thy;
put attributes directly on lemmas instead of using 'declare';
replace various 'lemmas' commands with ordinary 'lemma'.
huffman [Fri, 09 Dec 2011 14:52:51 +0100] rev 45804
remove redundant lemma word_diff_minus
huffman [Fri, 09 Dec 2011 14:14:05 +0100] rev 45803
remove some duplicate lemmas, simplify some proofs
kuncar [Fri, 09 Dec 2011 18:07:04 +0100] rev 45802
Quotient_Info stores only relation maps
bulwahn [Fri, 09 Dec 2011 16:08:32 +0100] rev 45801
hiding definitional facts in Quickcheck; introducing catch_match more honestly
kuncar [Fri, 09 Dec 2011 14:46:18 +0100] rev 45800
added dependencies
kuncar [Fri, 09 Dec 2011 14:22:05 +0100] rev 45799
added an example file with lifting of constants with contravariant and co/contravariant types
kuncar [Fri, 09 Dec 2011 14:16:42 +0100] rev 45798
merged
kuncar [Fri, 09 Dec 2011 14:14:37 +0100] rev 45797
make ctxt the first parameter
kuncar [Fri, 09 Dec 2011 14:12:02 +0100] rev 45796
context/theory parametres tuned
kuncar [Fri, 09 Dec 2011 14:03:17 +0100] rev 45795
maps are taken from enriched type infrastracture, rewritten lifting of constants, now we can lift even contravariant and co/contravariant types
huffman [Fri, 09 Dec 2011 13:42:16 +0100] rev 45794
add induction rule for list_all2
bulwahn [Fri, 09 Dec 2011 12:21:03 +0100] rev 45793
deactivating quickcheck_narrowing if Efficient_Nat theory is loaded
bulwahn [Fri, 09 Dec 2011 12:21:01 +0100] rev 45792
tuned quickcheck's response
noschinl [Fri, 09 Dec 2011 11:31:13 +0100] rev 45791
more systematic lemma name
bulwahn [Thu, 08 Dec 2011 13:53:28 +0100] rev 45790
adding examples for quickcheck narrowing about partial functions
bulwahn [Thu, 08 Dec 2011 13:53:27 +0100] rev 45789
removing special code generator setup for hd and last function because this causes problems with quickcheck narrowing as the Haskell Prelude functions throw errors that cannot be caught instead of PatternFail exceptions
huffman [Thu, 08 Dec 2011 13:46:04 +0100] rev 45788
HOLCF/ex/Letrec.thy: keep class 'domain' as default sort
huffman [Thu, 08 Dec 2011 13:25:54 +0100] rev 45787
more error checking for fixrec
huffman [Thu, 08 Dec 2011 13:25:40 +0100] rev 45786
reinstate old functions cfst and csnd as abbreviations
nipkow [Thu, 08 Dec 2011 09:10:54 +0100] rev 45785
merged
nipkow [Thu, 08 Dec 2011 09:10:44 +0100] rev 45784
tuned
Christian Urban <urbanc@in.tum.de> [Wed, 07 Dec 2011 16:06:08 +0000] rev 45783
merged
Christian Urban <urbanc@in.tum.de> [Wed, 07 Dec 2011 14:00:02 +0000] rev 45782
added a specific tactic and method that deal with partial equivalence relations
blanchet [Wed, 07 Dec 2011 16:03:05 +0100] rev 45781
use same order of facts for preplay as for actual reconstruction -- Metis sometimes exhibits very different timings depending on the order of the facts
blanchet [Wed, 07 Dec 2011 16:03:05 +0100] rev 45780
avoid multiple TFF1 declarations
blanchet [Wed, 07 Dec 2011 16:03:05 +0100] rev 45779
updated TFF1 support
blanchet [Wed, 07 Dec 2011 16:03:05 +0100] rev 45778
updated Metis to 20110926 version
hoelzl [Wed, 07 Dec 2011 15:10:29 +0100] rev 45777
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
huffman [Mon, 05 Dec 2011 15:10:15 +0100] rev 45776
remove mem_(c)ball_0 and centre_in_(c)ball from simpset, as rules mem_(c)ball always match instead
huffman [Wed, 07 Dec 2011 10:50:30 +0100] rev 45775
add cancellation simprocs for type enat
nipkow [Wed, 07 Dec 2011 11:24:45 +0100] rev 45774
tuned
bulwahn [Tue, 06 Dec 2011 15:23:16 +0100] rev 45773
increasing quickcheck's timeout in the example theory to avoid failures on the testing infrastructure
hoelzl [Tue, 06 Dec 2011 14:29:37 +0100] rev 45772
tuned proofs
nipkow [Tue, 06 Dec 2011 14:18:24 +0100] rev 45771
added lemmas
nipkow [Mon, 05 Dec 2011 22:29:43 +0100] rev 45770
tuned proof
hoelzl [Mon, 05 Dec 2011 17:33:57 +0100] rev 45769
real is better supported than real_of_nat, use it in the nat => ereal coercion
kuncar [Mon, 05 Dec 2011 14:47:01 +0100] rev 45768
merged
kuncar [Mon, 05 Dec 2011 14:44:46 +0100] rev 45767
the note about morphisms moved in the description part
bulwahn [Mon, 05 Dec 2011 12:36:28 +0100] rev 45766
updating documentation about quiet and verbose options in quickcheck
bulwahn [Mon, 05 Dec 2011 12:36:22 +0100] rev 45765
making the default behaviour of quickcheck a little bit less verbose;
adapting quickcheck examples
bulwahn [Mon, 05 Dec 2011 12:36:21 +0100] rev 45764
adding verbose configuration to quickcheck
bulwahn [Mon, 05 Dec 2011 12:36:20 +0100] rev 45763
random reporting compilation returns if counterexample is genuine or potentially spurious, and takes genuine_only option as argument
bulwahn [Mon, 05 Dec 2011 12:36:19 +0100] rev 45762
the reporting random testing also returns if the counterexample is genuine or potentially spurious
bulwahn [Mon, 05 Dec 2011 12:36:06 +0100] rev 45761
exhaustive returns if a counterexample is genuine or potentially spurious in the presence of assumptions more correctly
bulwahn [Mon, 05 Dec 2011 12:36:05 +0100] rev 45760
inverted flag potential to genuine_only in the quickcheck narrowing Haskell code
bulwahn [Mon, 05 Dec 2011 12:36:03 +0100] rev 45759
NEWS
bulwahn [Mon, 05 Dec 2011 12:36:02 +0100] rev 45758
documenting the genuine_only option in quickcheck;
bulwahn [Mon, 05 Dec 2011 12:36:00 +0100] rev 45757
renaming potential flag to genuine_only flag with an inverse semantics
bulwahn [Mon, 05 Dec 2011 12:35:58 +0100] rev 45756
quickcheck narrowing continues searching after found a potentially spurious counterexample
bulwahn [Mon, 05 Dec 2011 12:35:06 +0100] rev 45755
outputing the potentially spurious counterexample and continue search
bulwahn [Mon, 05 Dec 2011 12:35:05 +0100] rev 45754
dynamic genuine_flag in compilation of random and exhaustive
bulwahn [Mon, 05 Dec 2011 12:35:04 +0100] rev 45753
indicating where the restart should occur; making safe_if dynamic
nipkow [Mon, 05 Dec 2011 07:31:11 +0100] rev 45752
merged
nipkow [Mon, 05 Dec 2011 07:31:00 +0100] rev 45751
enforce parantheses around SKIP {_}
bulwahn [Sun, 04 Dec 2011 20:05:08 +0100] rev 45750
adding genuine flag to predicate_compile_quickcheck and prolog_quickcheck (cf. 5e46c225370e);
adjusting smart quickcheck compilation to new signature of exhaustive generators (cf. 1f5fc44254d7);
huffman [Sun, 04 Dec 2011 18:30:57 +0100] rev 45749
merged
huffman [Sun, 04 Dec 2011 13:10:19 +0100] rev 45748
remove Library/Diagonalize.thy, because Library/Nat_Bijection.thy includes all the same functionality
nipkow [Sun, 04 Dec 2011 18:29:29 +0100] rev 45747
missing dependency
nipkow [Sun, 04 Dec 2011 18:29:16 +0100] rev 45746
improved var names
nipkow [Sat, 03 Dec 2011 21:25:34 +0100] rev 45745
invariant holds before loop
wenzelm [Sat, 03 Dec 2011 13:11:50 +0100] rev 45744
caret_range based on BreakIterator, which handles combined unicode characters as well;
wenzelm [Fri, 02 Dec 2011 16:37:35 +0100] rev 45743
misc tuning;
wenzelm [Fri, 02 Dec 2011 16:24:48 +0100] rev 45742
some localization;
wenzelm [Fri, 02 Dec 2011 15:23:27 +0100] rev 45741
eliminated some legacy operations;
wenzelm [Fri, 02 Dec 2011 14:54:25 +0100] rev 45740
more antiquotations;
wenzelm [Fri, 02 Dec 2011 14:37:25 +0100] rev 45739
tuned whitespace;
wenzelm [Fri, 02 Dec 2011 14:26:43 +0100] rev 45738
eliminated some legacy operations;
wenzelm [Fri, 02 Dec 2011 13:59:25 +0100] rev 45737
removed dead code, which has never been active in recorded history;
wenzelm [Fri, 02 Dec 2011 13:51:36 +0100] rev 45736
do not open ML structures;
wenzelm [Fri, 02 Dec 2011 13:38:24 +0100] rev 45735
tuned signature;
huffman [Fri, 02 Dec 2011 10:31:47 +0100] rev 45734
hide quickcheck constants Abs_cfun and Rep_cfun, to avoid clash with HOLCF
bulwahn [Thu, 01 Dec 2011 22:16:26 +0100] rev 45733
hiding internal constants and facts more properly
bulwahn [Thu, 01 Dec 2011 22:16:23 +0100] rev 45732
removing catch_match' now that catch_match is polymorphic
bulwahn [Thu, 01 Dec 2011 22:14:35 +0100] rev 45731
adapting exhaustive generators in record package
bulwahn [Thu, 01 Dec 2011 22:14:35 +0100] rev 45730
outputing if counterexample is potentially spurious or not
bulwahn [Thu, 01 Dec 2011 22:14:35 +0100] rev 45729
making catch_match polymorphic
bulwahn [Thu, 01 Dec 2011 22:14:35 +0100] rev 45728
compilations return genuine flag to quickcheck framework
bulwahn [Thu, 01 Dec 2011 22:14:35 +0100] rev 45727
extending quickcheck's result by the genuine flag
bulwahn [Thu, 01 Dec 2011 22:14:35 +0100] rev 45726
reporting random compilation also catches match exceptions internally
bulwahn [Thu, 01 Dec 2011 22:14:35 +0100] rev 45725
the narrowing also indicates if counterexample is potentially spurious
bulwahn [Thu, 01 Dec 2011 22:14:35 +0100] rev 45724
the simple exhaustive compilation also indicates if counterexample is potentially spurious;
bulwahn [Thu, 01 Dec 2011 22:14:35 +0100] rev 45723
quickcheck-random compilation also indicates if the counterexample is potentially spurious or not
bulwahn [Thu, 01 Dec 2011 22:14:35 +0100] rev 45722
changing the exhaustive generator signatures;
replacing the hard-wired result type by its own identifier
bulwahn [Thu, 01 Dec 2011 22:14:35 +0100] rev 45721
quickcheck's compilation returns if it is genuine counterexample or a counterexample due to a match exception
bulwahn [Thu, 01 Dec 2011 22:14:35 +0100] rev 45720
adding examples for quickcheck-random
bulwahn [Thu, 01 Dec 2011 22:14:35 +0100] rev 45719
removing exception handling now that is caught at some other point;
tuned message
bulwahn [Thu, 01 Dec 2011 22:14:35 +0100] rev 45718
quickcheck random can also find potential counterexamples;
moved catch_match definition;
split quickcheck setup;
wenzelm [Thu, 01 Dec 2011 20:54:48 +0100] rev 45717
merged
nipkow [Thu, 01 Dec 2011 20:52:16 +0100] rev 45716
merged IMP/Util into IMP/Vars
hoelzl [Thu, 01 Dec 2011 15:41:58 +0100] rev 45715
use list theorems in Dining Cryptographers and Koepf Duermuth Countermeasure
hoelzl [Thu, 01 Dec 2011 15:41:58 +0100] rev 45714
cardinality of sets of lists
hoelzl [Thu, 01 Dec 2011 15:41:48 +0100] rev 45713
do not import examples Probability theory
hoelzl [Thu, 01 Dec 2011 14:03:57 +0100] rev 45712
moved theorems about distribution to the definition; removed oopsed-lemma
hoelzl [Thu, 01 Dec 2011 14:03:57 +0100] rev 45711
rename finite_prob_space.setsum_distribution, it collides with prob_space.setsum_distribution
hoelzl [Thu, 01 Dec 2011 14:03:57 +0100] rev 45710
remove duplicate theorem setsum_real_distribution
wenzelm [Thu, 01 Dec 2011 14:29:14 +0100] rev 45709
clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
blanchet [Thu, 01 Dec 2011 13:34:16 +0100] rev 45708
updated Sledgehammer docs with new/renamed options
blanchet [Thu, 01 Dec 2011 13:34:14 +0100] rev 45707
added "minimize" option for more control over automatic minimization