| Wed, 14 Dec 2011 12:18:19 +0100 |
wenzelm |
eliminated dead code;
|
changeset |
files
|
| Wed, 14 Dec 2011 12:10:44 +0100 |
wenzelm |
some full isatest runs, which include benchmark targets;
|
changeset |
files
|
| Wed, 14 Dec 2011 12:02:02 +0100 |
wenzelm |
more visible benchmarks;
|
changeset |
files
|
| Wed, 14 Dec 2011 10:18:28 +0100 |
blanchet |
fixed Nitpick definition of "<" on "real"s
|
changeset |
files
|
| Wed, 14 Dec 2011 08:32:48 +0100 |
huffman |
replace 'lemmas' with 'lemma'
|
changeset |
files
|
| Wed, 14 Dec 2011 07:38:30 +0100 |
huffman |
merged
|
changeset |
files
|
| Tue, 13 Dec 2011 18:33:04 +0100 |
huffman |
more simp rules for sbintrunc
|
changeset |
files
|
| Tue, 13 Dec 2011 15:34:59 +0100 |
huffman |
add simp rules for sbintrunc applied to numerals
|
changeset |
files
|
| Tue, 13 Dec 2011 14:39:14 +0100 |
huffman |
replace many uses of 'lemmas' with explicit 'lemma'
|
changeset |
files
|
| Tue, 13 Dec 2011 14:02:02 +0100 |
huffman |
add lemma bin_nth_zero
|
changeset |
files
|
| Tue, 13 Dec 2011 19:21:36 +0100 |
huffman |
add simp rules for bintrunc applied to numerals
|
changeset |
files
|
| Tue, 13 Dec 2011 13:21:48 +0100 |
huffman |
add simp rules for bin_rest and bin_last applied to numerals
|
changeset |
files
|
| Tue, 13 Dec 2011 13:10:25 +0100 |
huffman |
add simp rules for bin_sign applied to numerals
|
changeset |
files
|
| Tue, 13 Dec 2011 13:05:44 +0100 |
huffman |
add simp rules for BIT applied to numerals
|
changeset |
files
|
| Tue, 13 Dec 2011 12:55:36 +0100 |
huffman |
declare BIT_eq_iff [iff]; remove unneeded lemmas
|
changeset |
files
|
| Tue, 13 Dec 2011 12:36:41 +0100 |
huffman |
towards removing BIT_simps from the simpset
|
changeset |
files
|
| Tue, 13 Dec 2011 12:10:43 +0100 |
huffman |
type signature for bin_sign
|
changeset |
files
|
| Tue, 13 Dec 2011 12:05:47 +0100 |
huffman |
remove some unwanted numeral-representation-specific simp rules
|
changeset |
files
|
| Tue, 13 Dec 2011 11:48:59 +0100 |
huffman |
remove redundant lemmas
|
changeset |
files
|
| Tue, 13 Dec 2011 11:26:10 +0100 |
huffman |
reorder some definitions and proofs, in preparation for new numeral representation
|
changeset |
files
|
| Tue, 13 Dec 2011 23:22:27 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 13 Dec 2011 22:44:16 +0100 |
noschinl |
added lemmas
|
changeset |
files
|
| Tue, 13 Dec 2011 21:15:38 +0100 |
nipkow |
added concrete syntax
|
changeset |
files
|
| Tue, 13 Dec 2011 23:23:51 +0100 |
wenzelm |
'datatype' specifications allow explicit sort constraints;
|
changeset |
files
|
| Tue, 13 Dec 2011 20:29:59 +0100 |
wenzelm |
do not open ML structures;
|
changeset |
files
|
| Tue, 13 Dec 2011 20:10:36 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 13 Dec 2011 20:10:28 +0100 |
wenzelm |
removed dead code;
|
changeset |
files
|
| Tue, 13 Dec 2011 20:10:11 +0100 |
wenzelm |
comment;
|
changeset |
files
|
| Tue, 13 Dec 2011 16:53:28 +0100 |
nipkow |
connect while_option with lfp
|
changeset |
files
|
| Tue, 13 Dec 2011 16:14:41 +0100 |
nipkow |
lemmas about Kleene iteration
|
changeset |
files
|
| Tue, 13 Dec 2011 15:19:30 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 13 Dec 2011 14:55:42 +0100 |
blanchet |
avoid multiple type decls in TFF (improves on cef82dc1462d)
|
changeset |
files
|
| Tue, 13 Dec 2011 14:55:42 +0100 |
blanchet |
added missing quantifier
|
changeset |
files
|
| Tue, 13 Dec 2011 14:55:42 +0100 |
blanchet |
remove needless declaration in TFF1 problems
|
changeset |
files
|
| Tue, 13 Dec 2011 14:55:42 +0100 |
blanchet |
correctly declare implicit TFF1 types that appear first as type arguments with "$tType" and not "$i
|
changeset |
files
|
| Tue, 13 Dec 2011 15:18:52 +0100 |
wenzelm |
modernized specifications;
|
changeset |
files
|
| Tue, 13 Dec 2011 14:04:20 +0100 |
kuncar |
support phantom types as quotient types
|
changeset |
files
|
| Mon, 12 Dec 2011 23:06:41 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 12 Dec 2011 20:28:34 +0100 |
nipkow |
merged
|
changeset |
files
|
| Mon, 12 Dec 2011 20:28:19 +0100 |
nipkow |
tuned
|
changeset |
files
|
| Mon, 12 Dec 2011 23:05:21 +0100 |
wenzelm |
datatype dtyp with explicit sort information;
|
changeset |
files
|
| Mon, 12 Dec 2011 20:55:57 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 12 Dec 2011 19:47:50 +0100 |
wenzelm |
updated generated file;
|
changeset |
files
|
| Mon, 12 Dec 2011 17:22:48 +0100 |
bulwahn |
tuned quickcheck's response
|
changeset |
files
|
| Mon, 12 Dec 2011 13:45:54 +0100 |
bulwahn |
hiding constants and facts in the Quickcheck_Exhaustive and Quickcheck_Narrowing theory;
|
changeset |
files
|
| Mon, 12 Dec 2011 12:03:34 +0100 |
huffman |
merged
|
changeset |
files
|
| Mon, 12 Dec 2011 08:19:37 +0100 |
huffman |
replace more uses of 'lemmas' with explicit 'lemma';
|
changeset |
files
|
| Mon, 12 Dec 2011 15:32:54 +0900 |
Cezary Kaliszyk |
Add Quotient_Rat: an example of using the quotient package with partial equivalence relations, defining rational numbers.
|
changeset |
files
|
| Sun, 11 Dec 2011 21:57:22 +0100 |
huffman |
fix spelling
|
changeset |
files
|
| Sun, 11 Dec 2011 21:54:20 +0100 |
huffman |
fix spelling
|
changeset |
files
|
| Sun, 11 Dec 2011 18:22:06 +0100 |
nipkow |
added IMP/Live_True.thy
|
changeset |
files
|
| Sun, 11 Dec 2011 09:55:57 +0100 |
huffman |
replace many uses of 'lemmas' with 'lemma';
|
changeset |
files
|
| Sat, 10 Dec 2011 22:00:42 +0100 |
huffman |
prove class instances without extra lemmas
|
changeset |
files
|
| Sat, 10 Dec 2011 21:48:16 +0100 |
huffman |
finite class instance for word type; remove unused lemmas
|
changeset |
files
|
| Sat, 10 Dec 2011 21:07:59 +0100 |
huffman |
remove unused lemmas
|
changeset |
files
|
| Sat, 10 Dec 2011 16:24:22 +0100 |
huffman |
generalize some lemmas
|
changeset |
files
|
| Sat, 10 Dec 2011 13:00:58 +0100 |
huffman |
merged
|
changeset |
files
|
| Sat, 10 Dec 2011 08:29:19 +0100 |
huffman |
tidied Word.thy;
|
changeset |
files
|
| Fri, 09 Dec 2011 14:52:51 +0100 |
huffman |
remove redundant lemma word_diff_minus
|
changeset |
files
|
| Fri, 09 Dec 2011 14:14:05 +0100 |
huffman |
remove some duplicate lemmas, simplify some proofs
|
changeset |
files
|
| Fri, 09 Dec 2011 18:07:04 +0100 |
kuncar |
Quotient_Info stores only relation maps
|
changeset |
files
|
| Fri, 09 Dec 2011 16:08:32 +0100 |
bulwahn |
hiding definitional facts in Quickcheck; introducing catch_match more honestly
|
changeset |
files
|
| Fri, 09 Dec 2011 14:46:18 +0100 |
kuncar |
added dependencies
|
changeset |
files
|
| Fri, 09 Dec 2011 14:22:05 +0100 |
kuncar |
added an example file with lifting of constants with contravariant and co/contravariant types
|
changeset |
files
|
| Fri, 09 Dec 2011 14:16:42 +0100 |
kuncar |
merged
|
changeset |
files
|
| Fri, 09 Dec 2011 14:14:37 +0100 |
kuncar |
make ctxt the first parameter
|
changeset |
files
|
| Fri, 09 Dec 2011 14:12:02 +0100 |
kuncar |
context/theory parametres tuned
|
changeset |
files
|
| Fri, 09 Dec 2011 14:03:17 +0100 |
kuncar |
maps are taken from enriched type infrastracture, rewritten lifting of constants, now we can lift even contravariant and co/contravariant types
|
changeset |
files
|
| Fri, 09 Dec 2011 13:42:16 +0100 |
huffman |
add induction rule for list_all2
|
changeset |
files
|
| Fri, 09 Dec 2011 12:21:03 +0100 |
bulwahn |
deactivating quickcheck_narrowing if Efficient_Nat theory is loaded
|
changeset |
files
|
| Fri, 09 Dec 2011 12:21:01 +0100 |
bulwahn |
tuned quickcheck's response
|
changeset |
files
|
| Fri, 09 Dec 2011 11:31:13 +0100 |
noschinl |
more systematic lemma name
|
changeset |
files
|
| Thu, 08 Dec 2011 13:53:28 +0100 |
bulwahn |
adding examples for quickcheck narrowing about partial functions
|
changeset |
files
|
| Thu, 08 Dec 2011 13:53:27 +0100 |
bulwahn |
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
|
changeset |
files
|
| Thu, 08 Dec 2011 13:46:04 +0100 |
huffman |
HOLCF/ex/Letrec.thy: keep class 'domain' as default sort
|
changeset |
files
|
| Thu, 08 Dec 2011 13:25:54 +0100 |
huffman |
more error checking for fixrec
|
changeset |
files
|
| Thu, 08 Dec 2011 13:25:40 +0100 |
huffman |
reinstate old functions cfst and csnd as abbreviations
|
changeset |
files
|
| Thu, 08 Dec 2011 09:10:54 +0100 |
nipkow |
merged
|
changeset |
files
|
| Thu, 08 Dec 2011 09:10:44 +0100 |
nipkow |
tuned
|
changeset |
files
|
| Wed, 07 Dec 2011 16:06:08 +0000 |
Christian Urban |
merged
|
changeset |
files
|
| Wed, 07 Dec 2011 14:00:02 +0000 |
Christian Urban |
added a specific tactic and method that deal with partial equivalence relations
|
changeset |
files
|
| Wed, 07 Dec 2011 16:03:05 +0100 |
blanchet |
use same order of facts for preplay as for actual reconstruction -- Metis sometimes exhibits very different timings depending on the order of the facts
|
changeset |
files
|
| Wed, 07 Dec 2011 16:03:05 +0100 |
blanchet |
avoid multiple TFF1 declarations
|
changeset |
files
|
| Wed, 07 Dec 2011 16:03:05 +0100 |
blanchet |
updated TFF1 support
|
changeset |
files
|
| Wed, 07 Dec 2011 16:03:05 +0100 |
blanchet |
updated Metis to 20110926 version
|
changeset |
files
|
| Wed, 07 Dec 2011 15:10:29 +0100 |
hoelzl |
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
|
changeset |
files
|
| Mon, 05 Dec 2011 15:10:15 +0100 |
huffman |
remove mem_(c)ball_0 and centre_in_(c)ball from simpset, as rules mem_(c)ball always match instead
|
changeset |
files
|
| Wed, 07 Dec 2011 10:50:30 +0100 |
huffman |
add cancellation simprocs for type enat
|
changeset |
files
|
| Wed, 07 Dec 2011 11:24:45 +0100 |
nipkow |
tuned
|
changeset |
files
|
| Tue, 06 Dec 2011 15:23:16 +0100 |
bulwahn |
increasing quickcheck's timeout in the example theory to avoid failures on the testing infrastructure
|
changeset |
files
|
| Tue, 06 Dec 2011 14:29:37 +0100 |
hoelzl |
tuned proofs
|
changeset |
files
|
| Tue, 06 Dec 2011 14:18:24 +0100 |
nipkow |
added lemmas
|
changeset |
files
|
| Mon, 05 Dec 2011 22:29:43 +0100 |
nipkow |
tuned proof
|
changeset |
files
|
| Mon, 05 Dec 2011 17:33:57 +0100 |
hoelzl |
real is better supported than real_of_nat, use it in the nat => ereal coercion
|
changeset |
files
|
| Mon, 05 Dec 2011 14:47:01 +0100 |
kuncar |
merged
|
changeset |
files
|
| Mon, 05 Dec 2011 14:44:46 +0100 |
kuncar |
the note about morphisms moved in the description part
|
changeset |
files
|