Mercurial
Mercurial
>
repos
>
testboard
/ graph
summary

shortlog

changelog
 graph 
tags

bookmarks

branches

files

gz

help
less
more

(0)
30000
10000
3000
1000
300
100
60
+60
+100
+300
+1000
+3000
+10000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScriptenabled browsers.
more simp rules for sbintrunc
20111213, by huffman
add simp rules for sbintrunc applied to numerals
20111213, by huffman
replace many uses of 'lemmas' with explicit 'lemma'
20111213, by huffman
add lemma bin_nth_zero
20111213, by huffman
add simp rules for bintrunc applied to numerals
20111213, by huffman
add simp rules for bin_rest and bin_last applied to numerals
20111213, by huffman
add simp rules for bin_sign applied to numerals
20111213, by huffman
add simp rules for BIT applied to numerals
20111213, by huffman
declare BIT_eq_iff [iff]; remove unneeded lemmas
20111213, by huffman
towards removing BIT_simps from the simpset
20111213, by huffman
type signature for bin_sign
20111213, by huffman
remove some unwanted numeralrepresentationspecific simp rules
20111213, by huffman
remove redundant lemmas
20111213, by huffman
reorder some definitions and proofs, in preparation for new numeral representation
20111213, by huffman
merged
20111213, by wenzelm
added lemmas
20111213, by noschinl
added concrete syntax
20111213, by nipkow
'datatype' specifications allow explicit sort constraints;
20111213, by wenzelm
do not open ML structures;
20111213, by wenzelm
tuned;
20111213, by wenzelm
removed dead code;
20111213, by wenzelm
comment;
20111213, by wenzelm
connect while_option with lfp
20111213, by nipkow
lemmas about Kleene iteration
20111213, by nipkow
merged
20111213, by wenzelm
avoid multiple type decls in TFF (improves on cef82dc1462d)
20111213, by blanchet
added missing quantifier
20111213, by blanchet
remove needless declaration in TFF1 problems
20111213, by blanchet
correctly declare implicit TFF1 types that appear first as type arguments with "$tType" and not "$i
20111213, by blanchet
modernized specifications;
20111213, by wenzelm
support phantom types as quotient types
20111213, by kuncar
merged
20111212, by wenzelm
merged
20111212, by nipkow
tuned
20111212, by nipkow
datatype dtyp with explicit sort information;
20111212, by wenzelm
tuned;
20111212, by wenzelm
updated generated file;
20111212, by wenzelm
tuned quickcheck's response
20111212, by bulwahn
hiding constants and facts in the Quickcheck_Exhaustive and Quickcheck_Narrowing theory;
20111212, by bulwahn
merged
20111212, by huffman
replace more uses of 'lemmas' with explicit 'lemma';
20111212, by huffman
Add Quotient_Rat: an example of using the quotient package with partial equivalence relations, defining rational numbers.
20111212, by Cezary Kaliszyk
fix spelling
20111211, by huffman
fix spelling
20111211, by huffman
added IMP/Live_True.thy
20111211, by nipkow
replace many uses of 'lemmas' with 'lemma';
20111211, by huffman
prove class instances without extra lemmas
20111210, by huffman
finite class instance for word type; remove unused lemmas
20111210, by huffman
remove unused lemmas
20111210, by huffman
generalize some lemmas
20111210, by huffman
merged
20111210, by huffman
tidied Word.thy;
20111210, by huffman
remove redundant lemma word_diff_minus
20111209, by huffman
remove some duplicate lemmas, simplify some proofs
20111209, by huffman
Quotient_Info stores only relation maps
20111209, by kuncar
hiding definitional facts in Quickcheck; introducing catch_match more honestly
20111209, by bulwahn
added dependencies
20111209, by kuncar
added an example file with lifting of constants with contravariant and co/contravariant types
20111209, by kuncar
merged
20111209, by kuncar
make ctxt the first parameter
20111209, by kuncar
less
more

(0)
30000
10000
3000
1000
300
100
60
+60
+100
+300
+1000
+3000
+10000
tip