isabelle: Graph

Mercurial Mercurial > repos > isabelle / 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 +30000 tip

adding code attribute to enable evaluation of equality on multisets
2011-12-14, by bulwahn
merged
2011-12-14, by wenzelm
updated Sledgehammer/SMT docs
2011-12-14, by blanchet
tuned signature;
2011-12-14, by wenzelm
eliminated dead code;
2011-12-14, by wenzelm
some full isatest runs, which include benchmark targets;
2011-12-14, by wenzelm
more visible benchmarks;
2011-12-14, by wenzelm
fixed Nitpick definition of "<" on "real"s
2011-12-14, by blanchet
replace 'lemmas' with 'lemma'
2011-12-14, by huffman
merged
2011-12-14, by huffman
more simp rules for sbintrunc
2011-12-13, by huffman
add simp rules for sbintrunc applied to numerals
2011-12-13, by huffman
replace many uses of 'lemmas' with explicit 'lemma'
2011-12-13, by huffman
add lemma bin_nth_zero
2011-12-13, by huffman
add simp rules for bintrunc applied to numerals
2011-12-13, by huffman
add simp rules for bin_rest and bin_last applied to numerals
2011-12-13, by huffman
add simp rules for bin_sign applied to numerals
2011-12-13, by huffman
add simp rules for BIT applied to numerals
2011-12-13, by huffman
declare BIT_eq_iff [iff]; remove unneeded lemmas
2011-12-13, by huffman
towards removing BIT_simps from the simpset
2011-12-13, by huffman
type signature for bin_sign
2011-12-13, by huffman
remove some unwanted numeral-representation-specific simp rules
2011-12-13, by huffman
remove redundant lemmas
2011-12-13, by huffman
reorder some definitions and proofs, in preparation for new numeral representation
2011-12-13, by huffman
merged
2011-12-13, by wenzelm
added lemmas
2011-12-13, by noschinl
added concrete syntax
2011-12-13, by nipkow
'datatype' specifications allow explicit sort constraints;
2011-12-13, by wenzelm
do not open ML structures;
2011-12-13, by wenzelm
tuned;
2011-12-13, by wenzelm
removed dead code;
2011-12-13, by wenzelm
comment;
2011-12-13, by wenzelm
connect while_option with lfp
2011-12-13, by nipkow
lemmas about Kleene iteration
2011-12-13, by nipkow
merged
2011-12-13, by wenzelm
avoid multiple type decls in TFF (improves on cef82dc1462d)
2011-12-13, by blanchet
added missing quantifier
2011-12-13, by blanchet
remove needless declaration in TFF1 problems
2011-12-13, by blanchet
correctly declare implicit TFF1 types that appear first as type arguments with "$tType" and not "$i
2011-12-13, by blanchet
modernized specifications;
2011-12-13, by wenzelm
support phantom types as quotient types
2011-12-13, by kuncar
merged
2011-12-12, by wenzelm
merged
2011-12-12, by nipkow
tuned
2011-12-12, by nipkow
datatype dtyp with explicit sort information;
2011-12-12, by wenzelm
tuned;
2011-12-12, by wenzelm
updated generated file;
2011-12-12, by wenzelm
tuned quickcheck's response
2011-12-12, by bulwahn
hiding constants and facts in the Quickcheck_Exhaustive and Quickcheck_Narrowing theory;
2011-12-12, by bulwahn
merged
2011-12-12, by huffman
replace more uses of 'lemmas' with explicit 'lemma';
2011-12-12, by huffman
Add Quotient_Rat: an example of using the quotient package with partial equivalence relations, defining rational numbers.
2011-12-12, by Cezary Kaliszyk
fix spelling
2011-12-11, by huffman
fix spelling
2011-12-11, by huffman
added IMP/Live_True.thy
2011-12-11, by nipkow
replace many uses of 'lemmas' with 'lemma';
2011-12-11, by huffman
prove class instances without extra lemmas
2011-12-10, by huffman
finite class instance for word type; remove unused lemmas
2011-12-10, by huffman
remove unused lemmas
2011-12-10, by huffman
generalize some lemmas
2011-12-10, by huffman

less more | (0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip

isabelle